Same here. I feel like I should have looked at the language features more closely before getting started. Something should have jumped at me

I'm porting this Kata to Lean. How do I add the axiom of choice to the forbidden axioms?

Why deceitful?

Thanks!

I don't want to insist too much. I'd just add that rather than offerring this alternative because there's a different way of doing things, I'd say that if this is the best way of doing things in Idris, it is not in Lean. If learning Idris entails learning this approach, it is a more esoteric approach in Lean because there exists simpler ways.

I would also offer that, if the kata had first been authored in Lean, it might have ended up equally awkward for Idris users to solve the translation, if a faithful translation does indeed exist. This being said, I am new to the CodeWars community so i don't want to dictate priorities.

The issue here is that it means the definition is in Lean more complicated than necessary and it is not idiomatic. It might feel more natural to Idris users but not to Lean users. That's why I would suggest we change the Lean version.

Can't we use equations and well-founded recursion to define pow_sqr_aux?