vscode-idris
vscode-idris copied to clipboard
make-lemma seem don't work
Here is the example:
isOdd' : Nat -> Bool
isOdd' Z = ?isOdd'_rhs_1
isOdd' (S k) = ?isOdd'_rhs_2
when you put cursor in isOdd' make-lemma got
isOdd' : Nat -> Bool
isOdd' : Nat -> Bool
isOdd' Z = ?isOdd'_rhs_1
isOdd' (S k) = '_rhs_2
when you put cursor in rhs_2 make-lemma got Errors (0)