def Isotope.STm.App (Arity : Type u_1) [instArgs : Args Arity] : Lang Arity

Equations

• Isotope.STm.App Arity = { Val := Empty, Op := fun (x : Arity) => Unit }

def Isotope.STm.toExp {A : Type u_1} : STm (App ℕ) A → SExp A

Equations

• (Isotope.STm.sym a).toExp = Isotope.SExp.atom a
• (Isotope.STm.op a es).toExp = Isotope.SExp.par fun (i : Fin arity) => (es i).toExp

def Isotope.SExp.toTerm {A : Type u_1} : SExp A → STm (STm.App ℕ) A

Equations

• (Isotope.SExp.atom a).toTerm = Isotope.STm.sym a
• (Isotope.SExp.par es).toTerm = Isotope.STm.op () fun (i : Isotope.UArgs.Ix length) => (es i).toTerm

@[simp]

theorem Isotope.SExp.toTerm_toExp {A : Type u_1} (e : SExp A) : e.toTerm.toExp = e

@[simp]

theorem Isotope.STm.toExp_toTerm {A : Type u_1} (e : STm (App ℕ) A) : e.toExp.toTerm = e