blob: 98d4e5c9684500a88dbad5dc4f02acbb0af4427b (
plain)
1
2
3
4
5
6
7
8
9
|
Set Primitive Projections.
CoInductive R := mkR { p : unit }.
CoFixpoint foo := mkR tt.
Check (eq_refl tt : p foo = tt).
Check (eq_refl tt <: p foo = tt).
Check (eq_refl tt <<: p foo = tt).
|