search

idris-hackers / idris-vim

Idris mode for vim
221 stars 52 forks source link

Wrong type generated by `\l` #48

Open ghost opened 8 years ago

ghost commented 8 years ago

When following the tutorial here I was told to press \l to generate plus_commutes_S. This generated a function of the wrong type:

plus_commutes_S : (k : Nat) -> (m : Nat) -> (plus m k = plus k m) -> S (plus m k) = plus m (S k)

instead of

plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k).

\t gives the right type of ?plus_commutes_S before doing this. Any idea what's happening?

stephen-smith commented 7 years ago

Lifting a lemma out adds new parameters based on many (all?) local bindings. The TDD with Idris book recommends deleting the unnecessary parameters first thing.

I, too, find this behavior a little weird, but addressing it would probably be done as part of language development, instead of in the editor plugin.