diff --git a/ascii-syntax.md b/ascii-syntax.md new file mode 100644 index 0000000..84aca1e --- /dev/null +++ b/ascii-syntax.md @@ -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 |