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

16 lines
450 B
Text
Raw Permalink Normal View History

2015-05-29 22:49:10 +00:00
640.hlean:25:8: proof state
P : quotient S → Type,
2015-05-29 22:49:10 +00:00
c c' : C,
a : A
⊢ pathover P (quotient.rec (λ b, sorry) (λ b b' H, sorry) (f a unit.star)) (eq_of_rel S (S.Rmk a unit.star)) sorry
2015-05-29 22:49:10 +00:00
640.hlean:25:22: proof state
P : quotient S → Type,
2015-05-29 22:49:10 +00:00
c c' : C,
a : A
⊢ pathover P sorry (eq_of_rel S (S.Rmk a unit.star)) sorry
640.hlean:25:36: proof state
P : quotient S → Type,
2015-05-29 22:49:10 +00:00
c c' : C,
a : A
⊢ pathover P sorry (eq_of_rel S (S.Rmk a unit.star)) sorry