michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
lean2/tests/lean/771.lean.expected.out

2 lines
138 B
Text
Raw Permalink Normal View History

fix(frontends/lean/elaborator): closes #771 Produce nicer error message when type/goal is a metavariable and universe metavariables have already been instantiated with universe parameters.
2015-08-07 19:31:43 +00:00
771.lean:3:3: error: failed to synthesize placeholder, type is a unknown (i.e., it is a metavariable) (solution: provide type explicitly)
Reference in a new issue Copy permalink