typing_abstraction.dk 139 Bytes
Newer Older
Gaspard FEREY's avatar
Gaspard FEREY committed
1 2 3 4 5 6 7 8 9
#NAME abs.
A:Type.
y:A.
P:A->Type.
p:P y.
id: x:A -> P x -> P x.
def T: P y.
(; [ ] T --> (z => id z p) y. ;)
[ ] T --> (z:A => id z p) y.