def Esolangs.Cornucopia.Expr.const (name : String) : Expr

Equations

• Esolangs.Cornucopia.Expr.const name = Esolangs.Cornucopia.Expr.call name []

def Esolangs.Cornucopia.exprId : Expr

Equations

• Esolangs.Cornucopia.exprId = Esolangs.Cornucopia.Expr.arg 0

def Esolangs.Cornucopia.defId : Def

Equations

• Esolangs.Cornucopia.defId = { arity := 1, expr := Esolangs.Cornucopia.exprId }

def Esolangs.Cornucopia.exprLoop (name : String) : Expr

Equations

• Esolangs.Cornucopia.exprLoop name = Esolangs.Cornucopia.Expr.call name [Esolangs.Cornucopia.Expr.arg 0]

def Esolangs.Cornucopia.defLoop (name : String) : Def

Equations

• Esolangs.Cornucopia.defLoop name = { arity := 1, expr := Esolangs.Cornucopia.exprLoop name }

def Esolangs.Cornucopia.exprLoopSucc₁ (name : String) : Expr

Equations

• Esolangs.Cornucopia.exprLoopSucc₁ name = Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.succName [Esolangs.Cornucopia.Expr.call name [Esolangs.Cornucopia.Expr.arg 0]]

def Esolangs.Cornucopia.defLoopSucc₁ (name : String) : Def

Equations

• Esolangs.Cornucopia.defLoopSucc₁ name = { arity := 1, expr := Esolangs.Cornucopia.exprLoopSucc₁ name }

def Esolangs.Cornucopia.exprLoopSucc₂ (name : String) : Expr

Equations

• Esolangs.Cornucopia.exprLoopSucc₂ name = Esolangs.Cornucopia.Expr.call name [Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.succName [Esolangs.Cornucopia.Expr.arg 0]]

def Esolangs.Cornucopia.defLoopSucc₂ (name : String) : Def

Equations

• Esolangs.Cornucopia.defLoopSucc₂ name = { arity := 1, expr := Esolangs.Cornucopia.exprLoopSucc₂ name }

def Esolangs.Cornucopia.zero : Expr

Equations

• Esolangs.Cornucopia.zero = Esolangs.Cornucopia.Expr.const "0"

def Esolangs.Cornucopia.exprZero : Expr

Equations

• Esolangs.Cornucopia.exprZero = Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.subName [Esolangs.Cornucopia.zero, Esolangs.Cornucopia.zero]

def Esolangs.Cornucopia.defZero : Def

Equations

• Esolangs.Cornucopia.defZero = { arity := 0, expr := Esolangs.Cornucopia.exprZero }

def Esolangs.Cornucopia.one : Expr

Equations

• Esolangs.Cornucopia.one = Esolangs.Cornucopia.Expr.const "1"

def Esolangs.Cornucopia.exprOne : Expr

Equations

• Esolangs.Cornucopia.exprOne = Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.succName [Esolangs.Cornucopia.zero]

def Esolangs.Cornucopia.defOne : Def

Equations

• Esolangs.Cornucopia.defOne = { arity := 0, expr := Esolangs.Cornucopia.exprOne }

@[simp]

theorem Esolangs.Cornucopia.arity_defId : defId.arity = 1

@[simp]

theorem Esolangs.Cornucopia.expr_defId : defId.expr = exprId

@[simp]

theorem Esolangs.Cornucopia.wf_exprId {prog : Prog} : Expr.WF prog 1 exprId

theorem Esolangs.Cornucopia.wf_exprLoop {prog : Prog} {name : String} (h : prog.def? name = some (defLoop name)) : Expr.WF prog 1 (exprLoop name)

theorem Esolangs.Cornucopia.wf_exprLoopSucc₁ {prog : Prog} {name : String} [H : prog.WFBuiltins] (h : prog.def? name = some (defLoopSucc₁ name)) : Expr.WF prog 1 (exprLoopSucc₁ name)

theorem Esolangs.Cornucopia.wf_exprLoopSucc₂ {prog : Prog} {name : String} [H : prog.WFBuiltins] (h : prog.def? name = some (defLoopSucc₂ name)) : Expr.WF prog 1 (exprLoopSucc₂ name)

theorem Esolangs.Cornucopia.Expr.wf_const {prog : Prog} {name : String} {d : Def} {k : ℕ} (h₁ : prog.def? name = some d) (h₂ : d.arity = 0) : WF prog k (const name)

theorem Esolangs.Cornucopia.wf_zero {prog : Prog} {k : ℕ} (h : prog.def? "0" = some defZero) : Expr.WF prog k zero

theorem Esolangs.Cornucopia.wf_one {prog : Prog} {k : ℕ} (h : prog.def? "1" = some defOne) : Expr.WF prog k one

theorem Esolangs.Cornucopia.wf_exprZero {prog : Prog} [H : prog.WFBuiltins] {k : ℕ} (h : prog.def? "0" = some defZero) : Expr.WF prog k exprZero

theorem Esolangs.Cornucopia.wf_exprOne {prog : Prog} [H : prog.WFBuiltins] {k : ℕ} (h : prog.def? "0" = some defZero) : Expr.WF prog k exprOne