idris-vim
idris-vim copied to clipboard
Wrong type generated by `\l`
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?
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.