17 lines
479 B
Text
17 lines
479 B
Text
1870.lean:21:2-21:5: error: tactic 'rfl' failed, equality lhs
|
|
Zero.ofOfNat0
|
|
is not definitionally equal to rhs
|
|
{ zero := 1 }
|
|
⊢ Zero.ofOfNat0 = { zero := 1 }
|
|
1870.lean:26:2-26:11: error: tactic 'apply' failed, failed to unify
|
|
?a = ?a
|
|
with
|
|
Zero.ofOfNat0 = { zero := 1 }
|
|
case h.h
|
|
⊢ Zero.ofOfNat0 = { zero := 1 }
|
|
1870.lean:31:2-31:11: error: tactic 'apply' failed, failed to unify
|
|
?a = ?a
|
|
with
|
|
Zero.ofOfNat0 = { zero := 1 }
|
|
case h.h
|
|
⊢ Zero.ofOfNat0 = { zero := 1 }
|