lean2/tests/lean/check_expr.lean.expected.out

a :: l : list A
check_expr.lean:8:0: error: 1 unsolved subgoal
A : Type,
l : list A,
a b : A
⊢ list A
check_expr.lean:8:0: error: failed to add declaration 'foo' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
  ?M_1
feat(library/tactic): add "check_expr" tactic closes #486 2015-04-20 01:56:50 +00:00			`a :: l : list A`
			`check_expr.lean:8:0: error: 1 unsolved subgoal`
			`A : Type,`
			`l : list A,`
			`a b : A`
			`⊢ list A`
			`check_expr.lean:8:0: error: failed to add declaration 'foo' to environment, value has metavariables`
			`remark: set 'formatter.hide_full_terms' to false to see the complete term`
feat(frontends/lean): apply eta-reduction in postprocessing step Perhaps, we should add an option to disable this new feature. Remark: this commit makes commit 46d418a redundant. I'm keeping 46d418a because we may retract this commit in the future. 2015-06-10 23:26:32 +00:00			`?M_1`