Fixed

Fixed

Fixed

Fixed

Approved

Coq translation

You can use existsi instead of use.

Turns out I had to import tactic first. Now it works.

I'm new to Lean Codewars. I'm used to fill ∃ quantifiers with the use tactic, but the Codewars Lean doesn't seem to know it:

Solution.lean:3:4
unknown identifier 'use'
Solution.lean:3:4
don't know how to synthesize placeholder
context:
⊢ Type ?

How do I solve such a kata here on Codewars? My code works in my "regular" Lean environment.

This Kata is not compatible with Lean 3.20.c as of 08/10/2020

This Kata is not compatible with Lean 3.20.c as of 08/10/2020

This Kata is not compatible with Lean 3.20.c as of 08/10/2020

This Kata is not compatible with Lean 3.20.c as of 08/10/2020

Fixed.