Wrong type generated by \l

[ghost]

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]

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.