- a, b (generic alphabet variables)
- α, β (generic type parameters)
- c (char)
- eq (equal)
- ε (epsilon or empty string for regular expression or regular hedge grammar)
- f (function)
- G (grammar)
- ge (greater than or equal)
- gt (greater than)
- Γ (environment)
- h, h.* (hypothesis or property)
- i, j (indexes)
- ih, ih.* (inductive hypothesis)
- iff, Iff (if and only if)
- l, l[0-9]* (length variable name)
- l (length of a Vector)
- le (less than or equal)
- lt (less than)
- m (monad type variable)
- n (natural numbers of finite number variable names)
- n (natural number representing the number of non-terminals or production rules)
- ℕ (natural number type)
- ν (nullable function name)
- φ, ψ (generic predicate type parameter, phi/psi)
- Φ, Ψ (eval pred function, Phi/Psi: φ -> α -> Bool)
- r (regular expression variable names) (TODO: need two more? s is symbol, p and q are for predicates)
- p, q (predicates)
- Π (Pi type)
- ℝ (real number type)
- s (symbol variable name)
- σ (symbol type parameter)
- u, v (type universes)
- xs, ys, zs (generic list variable names)
- x, y, z (generic first element of a list variable name)
- Z, ℤ (integers)
- { n : Nat // n % 2 = 0 } (Subtype)
- <-> (iff and only iff)
- [] (empty list)
- / (or prop)
- /\ (and prop)
- ¬ (not prop)
- ∃ (exists)
- ∀ (forall)
- × (product type)
- , (product value)
- ⊕ (sum type)
- ⟦ ⟧ (denote)
- ∅ (emptyset for regular expression or regular hedge grammar)
- ⊢ (entails)
- ≈ (equivalent supported via HasEquiv class, which is implemented by Setoids)
- ~ (eqv or equivalent that does not yet implement HasEquiv)
- || (boolean or)
- && (boolean and)
- ⊥ (bottom)
- ⊤ (top)
- |=, ⊨ (relation, entailment)
- · (Regex.concat)
- | (Regex.or)
- (r)* (regular expression star constructor)