(version: development)

8 unicode

Here is a very short survey of the Unicode symbols used in Cedille, together with the shortcut to type them in the emacs mode.

\l

Produces λ (lambda), for anonymous functions

\L

Produces Λ (capital lambda), for anonymous functions taking in compile-time arguments (erased at run-time)

\r

Produces → (right arrow)

\a

Produces ∀ (forall), for quantification over terms which are erased at run-time, and also over type-level expressions

\P

Produces Π (capital pi), for dependent function types and for all type-level quantification (even over types)

\s

Produces ★ (black star), the kind of types

\.

Produces · (center dot), for applying a function (term- or type-level) to a type-level argument

\f

Produces ◂ (leftwards double arrow), for checking a term against a type, or type against a kind, at the top-level

\h

Produces ● (black circle), a hole representing a missing subterm

\k

Produces 𝒌 (math bold italic small k). All kind-level defined symbols must start with this character.

\i

Produces ι (iota), for dependent intersections

\=

Produces ≃ (asymptotically equal to), for propositional equality

\b

Produces β (beta), for proving propositional equalities which follow just by beta-eta reduction

\e

Produces ε (epsilon), for reducing the sides of an equation

\R

Produces ρ (rho), for rewriting with an equation

\F

Produces φ (phi), for proving that if t ≃ t’, and t has type T, then t’ also has type T

\y

Produces ς (lowercase final sigma), for proving t ≃ t’ from t’ ≃ t.

\t

Produces θ (theta), for elimination with a motive (of McBride)

\x

Produces χ (chi), for changing the form of the expected or computed classifier to a definitionally equivalent one