| | Some definitions of interest. |
|
| comment | Def Kind of comment: $kind == a |
|
| eval_factorization | Def   {a..b }(f) == i:{a..b}. if(i) |
| | | Thm*  a,b: , f:({a..b}  ). {a..b}(f)  |
|
| int_seg | Def {i..j} == {k:| i  k < j } |
| | | Thm* m,n:. {m..n} Type |
|
| int_upper | Def {i...} == {j:| ij } |
| | | Thm* n:. {n...} Type |
|
| nat | Def  == {i:| 0i } |
| | | Thm* Type |
|
| not | Def  A == A   False |
| | | Thm* A:Prop. (A) Prop |
|
| trivial_factorization | Def trivial_factorization(z)(i) == if i= z 1 else 0 fi |
| | | Thm* a,b:, z:{a..b}. trivial_factorization(z) {a..b} |
