| Some definitions of interest. |
|
hlist | Def hlist('a) == 'a List |
| | Thm* 'a:S. hlist('a) S |
|
rep_list | Def rep_list('a;l) == < n: . if n< ||l|| then l[n] else arb('a) fi ,||l||> |
| | Thm* 'a:S, l:'a List. rep_list('a;l) (  'a)  |
|
length | Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive) |
| | Thm* A:Type, l:A List. ||l||  |
| | Thm* ||nil||  |
| | Thm* 'a:Type, l:'a List. ||l||  |
|
nat | Def == {i: | 0 i } |
| | Thm* Type |
| | Thm* S |
|
pi2 | Def 2of(t) == t.2 |
| | Thm* A:Type, B:(A Type), p:(a:A B(a)). 2of(p) B(1of(p)) |
|
stype | Def S == {T:Type| x:T. True } |
| | Thm* S Type{2} |