diff --git a/ascii-syntax.md b/ascii-syntax.md index 84aca1e..96c0d03 100644 --- a/ascii-syntax.md +++ b/ascii-syntax.md @@ -1,15 +1,15 @@ 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 universe | ★, ★¹ | 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 | +| 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` |