lean2/tests/lean/cases_failure.hlean.expected.out

cases_failure.hlean:11:2: error:invalid 'cases' tactic, unification failed
auxiliary goal at time of failure
  A : Type,
  z : A,
  b r t l : z = z,
  s : square t b l r,
  e_3 : z = z
  ⊢ Π e_4 e_5 e_6 e_7,
      eq.rec (eq.rec (eq.rec (eq.rec (eq.rec (eq.rec (eq.rec s (refl z)) (refl z)) e_3) e_4) e_5) e_6)
        e_7 = square.ids →
      unit
proof state:
A : Type,
x y z : A,
t : x = y,
b : z = y,
l : x = z,
r : y = y,
s : square t b l r
⊢ unit
cases_failure.hlean:13:0: error: don't know how to synthesize placeholder
A : Type,
x y z : A,
t : x = y,
b : z = y,
l : x = z,
r : y = y,
s : square t b l r
⊢ unit
cases_failure.hlean:13: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
fix(library/tactic/inversion_tactic): type incorrect term being built by 'cases' tactic fixes #545 2015-04-21 02:24:52 +00:00			`cases_failure.hlean:11:2: error:invalid 'cases' tactic, unification failed`
			`auxiliary goal at time of failure`
			`A : Type,`
feat(library/tactic/inversion_tactic): clear variables that have been eliminated by cases tactic see discussion at: https://groups.google.com/forum/#!topic/lean-discuss/oyzgIqdMyNc 2015-05-03 02:33:59 +00:00			`z : A,`
fix(library/tactic/inversion_tactic): type incorrect term being built by 'cases' tactic fixes #545 2015-04-21 02:24:52 +00:00			`b r t l : z = z,`
			`s : square t b l r,`
			`e_3 : z = z`
chore(tests): mass-update for pp.binder_types false 2016-06-01 02:14:42 +00:00			`⊢ Π e_4 e_5 e_6 e_7,`
fix(library/tactic/inversion_tactic): type incorrect term being built by 'cases' tactic fixes #545 2015-04-21 02:24:52 +00:00			`eq.rec (eq.rec (eq.rec (eq.rec (eq.rec (eq.rec (eq.rec s (refl z)) (refl z)) e_3) e_4) e_5) e_6)`
			`e_7 = square.ids →`
			`unit`
			`proof state:`
			`A : Type,`
			`x y z : A,`
			`t : x = y,`
			`b : z = y,`
			`l : x = z,`
			`r : y = y,`
			`s : square t b l r`
			`⊢ unit`
			`cases_failure.hlean:13:0: error: don't know how to synthesize placeholder`
			`A : Type,`
			`x y z : A,`
			`t : x = y,`
			`b : z = y,`
			`l : x = z,`
			`r : y = y,`
			`s : square t b l r`
			`⊢ unit`
			`cases_failure.hlean:13: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`