rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

Update 'ascii syntax'

rhi 2023-11-04 08:36:51 -04:00
parent b899577e2b
commit 4aa53ca4e7
1 changed files with 13 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
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` |