| Some definitions of interest. |
|
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 |
|
prime_nats | Def Prime == {x:| prime(x) } |
|
nat | Def == {i:| 0i } |
| | Thm* Type |
|
prime_mset_complete | Def prime_mset_complete(f)(x) == if is_prime(x) f(x) else 0 fi |
| | Thm* f:(Prime). prime_mset_complete(f) |