2014-10-28 23:08:39 +00:00
|
|
|
unifier_bug.lean:7:0: error: type mismatch at application
|
|
|
|
|
heq.rec_on H rfl
|
|
|
|
|
term
|
|
|
|
|
rfl
|
|
|
|
|
has type
|
2016-01-09 20:32:18 +00:00
|
|
|
eq.rec_on (type_eq_of_heq H) a = eq.rec_on (type_eq_of_heq H) a
|
2014-10-28 23:08:39 +00:00
|
|
|
but is expected to have type
|
2016-01-09 20:32:18 +00:00
|
|
|
eq.rec_on (type_eq_of_heq H) a = b
|
