agda.fmt

% Agda Language
%format data = "\keyw{data}\;"
%format record = "\keyw{data}\;"
%format constructor = "\keyw{constructor}\;"
%format field = "\keyw{field}\;"
%format ; = "\keyw{;}\;"
%format with = "\;\keyw{with}\;"
%format let = "\;\keyw{let}\;"
%format in = "\;\keyw{in}\;"
%format where = "\;\keyw{where}\;"
%format module = "\keyw{module}"
%format open = "\keyw{open}"
%format private = "\keyw{private}"
%format renaming = "\keyw{renaming}"
%format public = "\keyw{public}"
%format postulate = "\keyw{postulate}\;"
%format abstract = "\keyw{abstract}"
%format import = "\keyw{import}"
%format infixl = "\keyw{infixl}"
%format infixr = "\keyw{infixr}"
%format infix = "\keyw{infix}"
%format rewrite = "\;\keyw{rewrite}\;"
%format mutual = "\keyw{mutual}"
%format forall = "\prefix{\keyw{\forall}}"
%format ._ = "{\texttt.}\!\keyw{\anonymous}"
%format . = "{\texttt.}\!\!"
%format _ = "\keyw{\anonymous}"
%format ? = "{?}"
%format shed (e) = "\shed{\{" e "\}}"

%format = = "\mathrel{\keyw{=}}"
%format ∀ = "\keyw{\forall}"
%format | = "\,\keyw{\vert}\,"
%format λ = "\prefix{\keyw{\lambda}}"
%format → = "\,\keyw{\rightarrow}\,"
%format : = "\mathrel{\keyw{:}}"
%format ... = "\mathord{\keyw{\ldots}}"
%format { = "\keyw{\{}"
%format } = "\keyw{\}}"
%format ( = "\keyw{(}"
%format ) = "\keyw{)}"
%format Set = "\type{Set}"
%format Set₀ = "\type{Set_0}"
%format Set₁ = "\type{Set_1}"
%format Set₂ = "\type{Set_2}"

% Greek
%format α = "\alpha"
%format α′ = "\alpha\Prime{}"
%format β = "\beta"
%format γ = "\gamma"
%format Λ = "\Lambda"
%format σ = "\sigma"
%format ρ = "\rho"
%format ρ′ = "\rho\Prime{}"
%format ρ″ = "\rho\PPrime{}"
%format ω = "\omega"
%format ω′ = "\omega\Prime{}"
%format ω″ = "\omega\PPrime{}"

% Decorated letters
%format a′ = "a\Prime{}"
%format a″ = "a\PPrime{}"
%format a‴ = "a\PPPrime{}"
%format b′ = "b\Prime{}"
%format b″ = "b\PPrime{}"
%format b‴ = "b\PPPrime{}"
%format c′ = "c\Prime{}"
%format c″ = "c\PPrime{}"
%format c‴ = "c\PPPrime{}"
%format e′ = "e\Prime{}"
%format e″ = "e\PPrime{}"
%format e‴ = "e\PPPrime{}"
%format h₀ = "h_0"
%format h₁ = "h_1"
%format h′ = "h\Prime{}"
%format h″ = "h\PPrime{}"
%format h‴ = "h\PPPrime{}"
%format l′ = "l\Prime{}"
%format l″ = "l\PPrime{}"
%format l‴ = "l\PPPrime{}"
%format r₀ = "r_0"
%format r₁ = "r_1"
%format r′ = "r\Prime{}"
%format r″ = "r\PPrime{}"
%format s₀ = "s_0"
%format s₁ = "s_1"
%format s′ = "s\Prime{}"
%format s″ = "s\PPrime{}"
%format t₀ = "t_0"
%format t₁ = "t_1"
%format t′ = "t\Prime{}"
%format t″ = "t\PPrime{}"
%format u′ = "u\Prime{}"
%format u″ = "u\PPrime{}"
%format v′ = "v\Prime{}"
%format v″ = "v\PPrime{}"
%format x′ = "x\Prime{}"
%format x″ = "x\PPrime{}"
%format x‴ = "x\PPPrime{}"
%format y′ = "y\Prime{}"
%format y″ = "y\PPrime{}"
%format y‴ = "y\PPPrime{}"
%format z′ = "z\Prime{}"
%format z″ = "z\PPrime{}"
%format z‴ = "z\PPPrime{}"

%if True
%format Level.zero = "{\!\!}"
%endif

% Coinduction
%format ∞ = "\type{\infty}"
%format ♯ = "\dstr{\sharp}"
%format ♯_ = "\dstr{\sharp\anonymous}"
%format ♭ = "\func{\flat}"

% Category.Functor
%format <$> = "\func{{<}\!{\$}\!{>}}"

% Function
%format id = "\func{id}"
%format ∘ = "\infix{\func{\circ}}"
%format flip = "\func{flip}"
%format ∶ = "\infix{\func{:}}"
%format const = "\func{const}"

% Data.Empty
%format ⊥ = "\type{\bot}"
%format ⊥-elim = "\func{\bot\text-elim}"

% Data.Unit
%format ⊤ = "\type{\top}"
%format tt = "\cons{tt}"

% Data.Bool
%format if = "\prefix{\func{if}}"
%format then = "\infix{\func{then}}"
%format else = "\infix{\func{else}}"

% Data.Sum
%format ⊎ = "\infix{\type{\uplus}}"
%format _⊎_ = "\type{\anonymous\uplus\anonymous}"
%format inj₁ = "\cons{in_L}"
%format inj₂ = "\cons{in_R}"

% Data.Product renaming (_,_ to _∧_) -- or _‚_? lhs2TeX doesn't like commas
%format Σ = "\type{\Sigma}"
%format × = "\infix{\!\type{\times}\!}"
%format _×_ = "\type{\anonymous{\times}\anonymous}"
% format ‚ = "\infix{\cons{,}}"
% format _‚_ = "\cons{\anonymous,\anonymous}"
%format ∧ = "\infix{\cons{{\wedge}}}"
%format _∧_ = "\cons{\anonymous{\wedge}\anonymous}"
%format ∃ = "\type{\exists}"
%format ∃₂ = "\type{\exists_2}"
%format ∃₃ = "\type{\exists_3}"
%format ∃₄ = "\type{\exists_4}"
%format proj₁ = "\func{proj_L}"
%format proj₂ = "\func{proj_R}"

% Data.Star
%format Star = "\type{Star}"
%format ε = "\cons{\varepsilon}"
%format ◅ = "\infix{\cons{\lhd}}"
%format _◅_ = "\cons{\anonymous{\lhd}\anonymous}"
%format ◅◅ = "\infix{\func{{\lhd}\!{\lhd}}}"
%format _◅◅_ = "\func{\anonymous{\lhd}\!{\lhd}\anonymous}"
%format Star.gmap = "\func{Star.gmap}"
%format Star.gfold = "\func{Star.gfold}"
%format Star.gfoldl = "\func{Star.gfoldl}"
%format Star.map = "\func{Star.map}"
%format Star.fold = "\func{Star.fold}"

% Data.Fin
%format Fin = "\type{Fin}"
%format _≟Fin_ = "\func{\anonymous{\stackrel?=}_{Fin}\!\anonymous}"
%format ≟Fin = "\infix{\func{{\stackrel?=}_{Fin}}}"

% Data.Nat
%format ℕ = "\type{\mathbb{N}}"
%format 0 = "\name{0}"
%format zero = "\cons{zero}"
%format suc = "\cons{suc}"
%format + = "\mathbin{\func{+}}"
%format _+_ = "\func{\anonymous{+}\anonymous}"
%format _≟ℕ_ = "\func{\anonymous{\stackrel?=}_{\mathbb{N}}\!\anonymous}"
%format ≟ℕ = "\infix{\func{{\stackrel?=}_{\mathbb{N}}}}"

% Data.List
%format List = "\type{List}"
%format ∷ = "\cons{::}"
%format _∷_ = "\cons{\anonymous{::}\anonymous}"
%format [ = "\cons{[}"
%format ] = "\cons{]}"
%format _++_ = "\func{\anonymous{+}\!\!{+}\anonymous}"
%format ++ = "\infix{\func{{+}\!\!{+}}}"

% Data.Vec
%format Vec = "\type{Vec}"
%format Vec.lookup = "\func{Vec.lookup}"
%format Vec.replicate = "\func{Vec.replicate}"

% Data.Maybe
%format Maybe = "\type{Maybe}"
%format just = "\cons{just}"
%format nothing = "\cons{nothing}"

% Relation.Nullary
%format ¬ = "\type{\lnot}"
%format yes = "\cons{yes}"
%format no = "\cons{no}"
%format Dec = "\type{Dec}"

% Relation.Nullary.Decidable
%format ⌊_⌋ = "\func{{\lfloor}\anonymous{\rfloor}}"
%format ⌊ = "\prefix{\func{{\lfloor}}}"
%format ⌋ = "\postfix{\func{{\rfloor}}}"

% Relation.Binary
%format Rel = "\type{Rel}"
%format REL = "\type{REL}"
%format Reflexive = "\type{Reflexive}"
%format Symmetric = "\type{Symmetric}"
%format Sym = "\type{Sym}"
%format Transitive = "\type{Transitive}"
%format _⇒_ = "\type{\anonymous{\Rightarrow}\anonymous}"
%format ⇒ = "\infix{\type{{\Rightarrow}}}"
%format _Preserves₂_⟶_⟶_ = "\type{\anonymous{}Preserves_2\anonymous{\longrightarrow}\anonymous{\longrightarrow}\anonymous}"
%format Preserves₂ = "\infix{\type{Preserves_2}}"

% Relation.Binary.PropositionalEquality
%format _≡_ = "\type{\anonymous{\equiv}\anonymous}"
%format ≡ = "\infix{\type{\equiv}}"
%format ≡.refl = "\cons{{\equiv}.refl}"
%format ≡.trans = "\func{{\equiv}.trans}"
%format ≡.sym = "\func{{\equiv}.sym}"
%format ≢ = "\infix{\type{\not\equiv}}"
%format ≡.cong = "\func{{\equiv}.cong}"
%format ≡.inspect = "\func{{\equiv}.inspect}"
%format with-≡ = "\infix{\cons{with\text-{\equiv}}}"
%format ≗ = "\infix{\type{\circeq}}"

% Relation.Binary.PreorderReasoning
%format begin = "\func{begin}"
%format _≡⟪_⟫_ = "\func{\anonymous{\equiv}\langle\anonymous\rangle\anonymous}"
%format _≈⟪_⟫_ = "\func{\anonymous{\approx}\langle\anonymous\rangle\anonymous}"
%format _≈⟪_⁻¹⟫_ = "\func{\anonymous{\approx}\langle\anonymous{}^{\text-1}\rangle\anonymous}"
%format ⟪ = "\func{\langle}"
%format ≈⟪ = "\func{{\approx}\langle}"
%format ≡⟪ = "\func{{\equiv}\langle}"
%format ⟫ = "\func{\rangle}"
%format ⁻¹⟫ = "\func{{}^{\text-1}\rangle}"
%format ∎ = "\func{\rule{1ex}{1ex}}"