Expression Syntax

Functions

In mathematical expressions, you can choose whether to call functions in a more functional-language style with f x y or a more imperative-language style with f (x,y). This is because , is syntactic sugar that compiles to )(.

Sets

Sets are represented using predicates. Instead of saying “x is in the set of natural numbers”, we have an “is a natural number” predicate, Nat, and then say that it applies to x, Nat x.

Infix Notation

There are three built-in infix operators, _ and _, _ or _, and _ = _. All user-defined expressions are prefix, e.g. + _ _.

If

If statements in this language are often called implication in other languages. When we write if P then Q, we are saying that P implies Q, or whenever P holds, Q also holds.

Bi-Implication

To denote (if P then Q) and (if Q then P), you can write P = Q. (There is no difference between equality and bi-implication in this language.)

Quantifiers

There are two quantifiers in this language: forall _ . _ and exists _ . _.

forall A B . if A then if B then A

exists x y. P(x,y)

You can specify sets that the new identifiers belong to using ::

forall x y : Nat, a b : Bool, P. if P(x,a) then P(y,b)

Anonymous Functions

Anonymous function (lambdas) are speficied using fun _ . _. Like quantifiers you can specify multiple identifiers, but unlike quantifiers you cannot specify that the arguments belong to a certain set.

(fun x y. + 2 (+ x y)) (5,5) = 12

Negation

The ¬ symbol denotes negation.

¬ (3 = 4)

Set Shorthand

In cases where it would be easier to read n : Nat can be written instead of Nat n to indicate set membership. Below some shorthands are shown, with their equivalents below:

xs : List Nat
List Nat xs

f : Nat -> Nat -> Nat
forall T. if Nat T then forall T'. if nat T' then Nat(f(T, T'))

[] : forall x. List x
forall x. List x []