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