3 lines
107 B
Text
3 lines
107 B
Text
|
858.lean:2:2: error: failed to add declaration 'n' to local context, type has metavariables
|
|||
|
?M_1 → ℕ
|