| Some definitions of interest. |
|
prime_nats | Def Prime == {x: | prime(x) } |
|
nat | Def == {i: | 0 i } |
| | 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)     |
|
prime_decider | Def is_prime(x) == prime_decider_exists{1:l}(x) |
| | Thm* x: . is_prime(x)  |