lean2/tests/lean/assert_fail.lean.expected.out

assert_fail.lean:4:0: error: 2 unsolved subgoals
a b : Prop,
H : b ∧ a
⊢ a

a b : Prop,
H : b ∧ a,
H : a
⊢ a ∧ b
assert_fail.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
  ?M_1
assert_fail.lean:9:2: error:invalid tactic, there are no goals to be solved
proof state:
no goals
assert_fail.lean:10:0: error: don't know how to synthesize placeholder
a : Prop,
Ha : a
⊢ a
assert_fail.lean:10:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
  ?M_1
feat(library/tactic/assert_tactic): allow duplicate names for hypotheses in assert tactic 2015-07-23 18:15:24 -07:00			`assert_fail.lean:4:0: error: 2 unsolved subgoals`
feat(library/tactic): produce better error message when a tactic fails closes #348 2015-02-16 16:56:42 -08:00			`a b : Prop,`
			`H : b ∧ a`
feat(library/tactic/assert_tactic): allow duplicate names for hypotheses in assert tactic 2015-07-23 18:15:24 -07:00			`⊢ a`

feat(library/tactic): produce better error message when a tactic fails closes #348 2015-02-16 16:56:42 -08:00			`a b : Prop,`
feat(library/util): disable local constant purification when pretty printing goals This feature generates confusion. 2015-07-23 18:43:56 -07:00			`H : b ∧ a,`
fix(library/util): incorrect hypothesis renaming when pretty printing goals 2015-07-23 18:38:35 -07:00			`H : a`
feat(library/tactic): produce better error message when a tactic fails closes #348 2015-02-16 16:56:42 -08:00			`⊢ a ∧ b`
feat(frontends/lean/decl_cmds): avoid funny names when displaying error messages for "examples" 2015-06-01 15:35:28 -07:00			`assert_fail.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables`
feat(frontends/lean): hide subterms that do not contain metavariables when generating "unresolved metavariables" error message closes #473 2015-03-13 12:42:57 -07:00			`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 16:26:32 -07:00			`?M_1`
feat(library/tactic): produce better error message when a tactic fails closes #348 2015-02-16 16:56:42 -08:00			`assert_fail.lean:9:2: error:invalid tactic, there are no goals to be solved`
			`proof state:`
			`no goals`
			`assert_fail.lean:10:0: error: don't know how to synthesize placeholder`
			`a : Prop,`
			`Ha : a`
			`⊢ a`
feat(frontends/lean/decl_cmds): avoid funny names when displaying error messages for "examples" 2015-06-01 15:35:28 -07:00			`assert_fail.lean:10:0: error: failed to add declaration 'example' to environment, value has metavariables`
feat(frontends/lean): hide subterms that do not contain metavariables when generating "unresolved metavariables" error message closes #473 2015-03-13 12:42:57 -07:00			`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 16:26:32 -07:00			`?M_1`