to a Prop is normally invisible since it is pretty obvious when it is needed.| NOTE: | This operator coercing a to a Prop is normally invisible since it is pretty obvious when it is needed. |
| Who Cites assert? | |
| assert | Def  b == if b True else False fi |
Thm*  b:. b  Prop | |
| eq_bool | Def p= q == (p q)  ( pq) |
| Thm* p,q:. p=q | |
| iff | Def P   Q == (P  Q) & (P Q) |
| Thm* A,B:Prop. (A B) Prop | |
| bnot | Def b == if b false else true fi |
| Thm* b:. b | |
| band | Def pq == if p q else false fi |
| Thm* p,q:. (pq) | |
| bor | Def p q == if p true else q fi |
| Thm* p,q:. (p q) | |
| rev_implies | Def P Q == Q P |
| Thm* A,B:Prop. (A B) Prop |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |