| Some definitions of interest. |
|
compose | Def (f o g)(x) == f(g(x)) |
| | Thm* A,B,C:Type, f:(BC), g:(AB). f o g AC |
|
sfa_doc_indscheme | Def Induction for x:. P(x) == P(0) & (x:. P(x) P(x+1)) (x:. P(x)) |
|
nat | Def == {i:| 0i } |
| | Thm* Type |
|
le | Def AB == B<A |
| | Thm* i,j:. (ij) Prop |
|
not | Def A == A False |
| | Thm* A:Prop. (A) Prop |
|
sfa_doc_le_parm_sample_def | Def HigherConsequence{i}(P) == {X:Prop{i'}| P X } |
|
sfa_doc_tok_num_literal | Def $abc.$n == <"$abc",$n> |
|
sfa_doc_weird_def | Def Weird(x; u,v. F(u;v)) == F(F(x;0);x) |