| Some definitions of interest. |
|
hfun | Def 'a  'b == 'a 'b |
| | Thm* 'a,'b:S. ('a  'b) S |
|
nat | Def == {i: | 0 i } |
| | Thm* Type |
| | Thm* S |
|
ncompose | Def ncompose(f;n;x) == if n= 0 then x else f(ncompose(f;n-1;x)) fi (recursive) |
| | Thm* 'a:Type, n: , x:'a, f:('a 'a). ncompose(f;n;x) 'a |
|
stype | Def S == {T:Type| x:T. True } |
| | Thm* S Type{2} |