- a !
a + a
not a = a
not a + a
not s a + a
not s n <= 0
def s n <= 0
not a => b
not s a => s b
def a = b
10 * b (n div 10)
10 when n < 10 else 10 * b (n div 10)
m (m, n) = m when m <= n else n
(i div p) < (j div q) <=> (i * q) < (j * p)
f + - f = f
- f + - f + - f = - f + - f + - f
f a none a but f a
f a one a done
f a --> f a
s a <= 0
not if if a then b else c then b else c
a when (exists a : Unit . true) else b
(a * b) ::: a b = a ::: b
f (- b)
a = b <=> b = a
a - b = b - a
(a => b) = (b if a)
(a ::: b) + (a ::: b)
(a + b) ::: (a + b)
a =e= b
(a =e= b) = (a =e= b)
(a = b) =e= (a = b)
- forall a : Unit . true /\ exists b : Unit . false
if (exists a : Unit . 1) then (exists a : Unit . 1) else 0
exists a : Unit . true if true
(exists a : Unit . true) if true
not p = not q
def not a = a
a = not a
a + def a