| Some definitions of interest. |
|
comment | Def Kind of comment: $kind == a |
|
prime | Def prime(a) == a = 0 & (a ~ 1) & (b,c:. a | bc a | b a | c) |
| | Thm* a:. prime(a) Prop |
|
divides | Def b | a == c:. a = bc |
| | Thm* a,b:. (a | b) Prop |
|
int_seg | Def {i..j} == {k:| i k < j } |
| | Thm* m,n:. {m..n} Type |
|
nat | Def == {i:| 0i } |
| | Thm* Type |