b == if b
True else False fi
b:
. b 
Prop
a,v. if P(a) [a / v] else v fi;nil;l)T:Type, P:(T
), l:T List. filter(P;l) T List
l2 == 
l:T List. l2 = (l1 @ l)T:Type, l1,l2:T List. l1 l2 Prop
A == A 
FalseA:Prop. (A) Prop| Some definitions of interest. | |
| assert | b == if b True else False fi |
| b:. b Prop | |
| filter | a,v. if P(a) [a / v] else v fi;nil;l) |
| T:Type, P:(T), l:T List. filter(P;l) T List | |
| iseg | l2 == l:T List. l2 = (l1 @ l) |
| T:Type, l1,l2:T List. l1 l2 Prop | |
| not | A == A False |
| A:Prop. (A) Prop |
About:
 |  |  |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |  |