| Some definitions of interest. |
|
hel | Def el == n: . l:'a List. if n= 0 then hd(l) else el(n-1,tl(l)) fi
Def (recursive) |
| | Thm* 'a:S. el (hnum  hlist('a)  'a) |
|
hfun | Def 'a  'b == 'a 'b |
| | Thm* 'a,'b:S. ('a  'b) S |
|
hlist | Def hlist('a) == 'a List |
| | Thm* 'a:S. hlist('a) S |
|
nat | Def == {i: | 0 i } |
| | Thm* Type |
| | Thm* S |
|
stype | Def S == {T:Type| x:T. True } |
| | Thm* S Type{2} |
|
tlambda | Def ( x:T. b(x))(x) == b(x) |