------------------------------------------------------------------------
-- Various constants
------------------------------------------------------------------------

open import Atom

module Constants (atoms : χ-atoms) where

open χ-atoms atoms

c-zero : Const
c-zero = C.name 

c-suc : Const
c-suc = C.name 

c-nil : Const
c-nil = C.name 

c-cons : Const
c-cons = C.name 

c-apply : Const
c-apply = C.name 

c-case : Const
c-case = C.name 

c-rec : Const
c-rec = C.name 

c-lambda : Const
c-lambda = C.name 

c-const : Const
c-const = C.name 

c-var : Const
c-var = C.name 

c-branch : Const
c-branch = C.name 

c-true : Const
c-true = C.name 

c-false : Const
c-false = C.name 

c-pair : Const
c-pair = C.name 

v-equal : Var
v-equal = V.name 

v-m : Var
v-m = V.name 

v-n : Var
v-n = V.name 

v-x : Var
v-x = V.name 

v-new : Var
v-new = V.name 

v-e : Var
v-e = V.name 

v-subst : Var
v-subst = V.name 

v-e₁ : Var
v-e₁ = V.name 

v-e₂ : Var
v-e₂ = V.name 

v-bs : Var
v-bs = V.name 

v-y : Var
v-y = V.name 

v-c : Var
v-c = V.name 

v-es : Var
v-es = V.name 

v-ys : Var
v-ys = V.name 

v-member : Var
v-member = V.name 

v-xs : Var
v-xs = V.name 

v-lookup : Var
v-lookup = V.name 

v-b : Var
v-b = V.name 

v-c′ : Var
v-c′ = V.name 

v-underscore : Var
v-underscore = V.name 

v-substs : Var
v-substs = V.name 

v-e′ : Var
v-e′ = V.name 

v-map : Var
v-map = V.name 

v-p : Var
v-p = V.name 

v-eval : Var
v-eval = V.name 

v-internal-code : Var
v-internal-code = V.name 

v-halts : Var
v-halts = V.name 

v-z : Var
v-z = V.name 

v-f : Var
v-f = V.name 

v-g : Var
v-g = V.name