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:34:15 -04:00
parent 79370a6058
commit b899577e2b
1 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
ascii-syntax.md Normal file

@ -0,0 +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 |