2015-03-27 21:47:13 +00:00
|
|
|
487.hlean:18:56: error: 1 unsolved subgoal
|
2015-03-24 01:29:30 +00:00
|
|
|
A : Type,
|
|
|
|
|
B : Type,
|
|
|
|
|
f : A → B,
|
|
|
|
|
g : B → A,
|
2016-06-01 02:14:42 +00:00
|
|
|
ε : Π b, f (g b) = b,
|
2015-03-24 01:29:30 +00:00
|
|
|
b b' : B
|
2015-05-18 22:40:43 +00:00
|
|
|
⊢ (ε b)⁻¹ ⬝ ε b = refl b
|
2015-03-24 01:29:30 +00:00
|
|
|
487.hlean:19: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
|
2016-06-01 02:14:42 +00:00
|
|
|
λ A B f g ε b b',
|
2015-03-24 01:29:30 +00:00
|
|
|
is_retraction.mk … ?M_1
|
