Unicode

Unicode syntax examples

Open in Workbench View on GitHub

1-- Unicode syntax examples2-- Part of the Grace17 proof assistant for mathematics based on set theory.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67-- Unicode and ASCII spellings elaborate to the same kernel syntax.89def διπλό (ν : ℕ) → ℕ10  | 0 ⇒ 011  | succ(κ) ⇒ succ(succ(διπλό(κ)))1213theorem διπλό.correct (ν : ℕ)14  shows διπλό(ν) = ν + ν15proof16  induction ν17  | 0 => settle with διπλό, plus18  | succ(κ) using ih => settle with διπλό, plus, plus.succ_right, ih1920theorem pair.both_unicode (α β : Set)21  shows α ∈ pair(α, β) ∧ β ∈ pair(α, β)22proof23  settle with pair.membership2425theorem equality.exists_unicode (α : Set)26  shows ∃ β, β = α27proof28  witness α ⇒ settle2930theorem equality.iff_unicode (α : Set)31  shows α = α ↔ α = α32proof33  settle3435theorem epsilon0.less.unicode (α β : Set)36  shows relates(ε₀.less, α, β) ↔ α ∈ ε₀ ∧ β ∈ ε₀ ∧ α ∈ β37proof38  settle with epsilon0.less.membership3940theorem logic.unicode_quantifiers (α : Set)41  shows ∀ γ, γ = γ ∨ ¬(α ≠ α)42proof43  settle4445theorem logic.unicode_implication (α : Set)46  shows α = α → α = α47proof48  settle49