i like the full-unicode syntax better so i use it in examples, but it's not mandatory. you can give the compiler the --ascii flag to print error messages this way.
| what | full unicode | ascii only |
|---|---|---|
| type universes | ★; ★¹ |
Type; Type1 or Type^1 |
| universe displacement | f¹ |
f^1 |
| natural type | ℕ |
Nat |
| ω suffix on keywords | caseω, defω, etc |
case#, def#, … |
| function types | ω.(a : A) → B a |
#.(a : A) -> B a |
| function values | λ x ⇒ e |
fun x => e |
| pair types | (a : A) × B a |
(a : A) ** B a |
| case expressions | case … of { p ⇒ e } |
case … of { p => e } |
| equality types | a ≡ b : A |
a == b : A |
| equality proofs | δ i ⇒ e |
dfun i => e |
| inline type annotations | e ∷ A |
e :: A |