(pred y : bb)

(pred y : bb * bb)

(pred y : bb * bb)(a, b)

(pred y : bb * bb) a b

Error (line 4, column 1) no resolution for term: (pred y:bb*bb) a b

a =e= < b

Error (line 5, column 7) unexpected mixfix token: <

a #= e = b

Error (line 6, column 3) unexpected mixfix token: #=

exists1 (predy :: bb)

Error (line 7, column 1) unexpected mixfix token: exists1

Error (line 7, column 10) unexpected mixfix token: predy

exists predy:bb . a

exists! a:v . x

exists! a:v . x

exists! a:v . x

forall a:v . x

b => a

def x

def #

Error (line 15, column 4) unexpected mixfix token: #

{} when [] else {}

Error (line 16, column 2) unexpected mixfix token: }

Error (line 16, column 7) not a predicate: []

Error (line 16, column 14) unexpected mixfix token: }

Error (line 16, column 3) not a formula: {} when [] else {}

a /\ b /\ c

a \/ b \/ c

a => b

a <=> b

true

false

b in s

a =e= b

a = b

a => b => c => d

d => c => b => a

a <=> b

(def d) => not c => b \/ c => a /\ b

m div n = r <=> exists s:Nat . m = n * r + s /\ s < n