y:
. x<y 
f(y) = 0 
x:, f:(
). f zero beyond x Prop == {i:
| 0
i } Type
(i rem 2)i:. i even 
b
b else a fia,b:. max(a;b) | Some definitions of interest. | |
| sfa_doc_props_as_types_example1 | y:. x<y f(y) = 0 |
| x:, f:(). f zero beyond x Prop | |
| nat | == {i:| 0i } |
| Type | |
| sfa_doc_even | (i rem 2) |
| i:. i even | |
| sfa_doc_max_int | b b else a fi |
| a,b:. max(a;b) |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |