*
**
a_a
__
123
1.2
1
1.2E3
12.23E34
"bla"
""
=
<
<=
.a
'a'
= [a, b]
< [a, b]
<= [a, b]
.a [a, b]
'a' [a, b]
__ * __
a =e= b
a = e = b
a = e = b
a = e = __ b __
(a = b)
(a __ b)
(a __ b) a
b (a __ b)
b (a __ b) a
{a __ b}
{a __ b} a
b {a __ b}
b {a __ b} a
[a __ b]
[a __ b] a
b [a __ b]
b [a __ b] a
(a, =, b)
({}, [], {[] {}})
{{}, [], {[] {}}}
[{}, [], {[] {}}]
((var y : bb))
((op y : bb))
((op __<__ : ##))
((op __<__ : ## -> --))
((op __<__ : bb))
((op __<__ : ? bb))
((op __<__ : ? ##))
((pred y : bb))
((pred y : bb * bb))
((var y : bb -> bb))
a = e =< b
ys as b
((pred y : bb))
((pred y : bb))
((pred y : ()))
(predy y : bb)
(predy : bb)
(predy : bb)
exists1 (predy :: bb)
exists predy : bb . a
exists! a : v . x
exists! a : v . x
exists! # : v . x
forall a : v . x
\ a : v . x
\ a : v . x
\ a : v .! x
\ a : v .! x
\ a : v . ! x
\ a : v . ! x
a if b
a when b else c
def x
def #
{} when [] else {}
a /\ b /\ c
a \/ b \/ c
a => b
a <=> b
true
false
# as b
b in #
a \ a : v .! ! x
= e =
= e <
= e <
= ea
= e a
= a =
= a =
== e =
== e =
=e= e =e=
=e= e =e=
= e =e= e =
((op __<__ : ? ## -> bb))
((op __<__ : ? aa * bb))
let x = y in z
let x = y; x = y; x = y in z
let x = y; x = y; x = y in z in t
let x = (y in z) in x
let x = \ y : t . y in x (x)
let x = case x in t of y -> z; x = y in x
()
if a then b
a if b
if a then b else c
(a, b) as t
((a, b) as t)
\ (a @ (b, c) : S * S) . a
\ (a # (b, c) : S * S) . a
\ (a # (b, c) # : S * S) . a
\ (a) . a
y where x = y; z = y
y where x = y; z = y in t
((op __<__ : ?##))
((op __<__ : ? ##))