def Esolangs.Cornucopia.ProgLoopSucc₂.defs : List (String × Def)

Equations

• Esolangs.Cornucopia.ProgLoopSucc₂.defs = [(Esolangs.Cornucopia.mainName, { arity := 1, expr := Esolangs.Cornucopia.exprLoopSucc₂ Esolangs.Cornucopia.mainName })]

def Esolangs.Cornucopia.ProgLoopSucc₂.fs (n : ℕ) : Map String (List ℕ → ℕ)

Equations

• Esolangs.Cornucopia.ProgLoopSucc₂.fs n = Map.ofList [(Esolangs.Cornucopia.mainName, Esolangs.Cornucopia.fn 1 fun (x : List ℕ) => n)]

def Esolangs.Cornucopia.ProgLoopSucc₂.prog : Prog

Equations

• Esolangs.Cornucopia.ProgLoopSucc₂.prog = Esolangs.Cornucopia.Prog.ofDefs Esolangs.Cornucopia.ProgLoopSucc₂.defs

@[simp]

theorem Esolangs.Cornucopia.ProgLoopSucc₂.nodup_defs : (List.map (fun (x : String × Def) => x.1) defs).Nodup

@[simp]

instance Esolangs.Cornucopia.ProgLoopSucc₂.wfBuiltins_prog : prog.WFBuiltins

@[simp]

theorem Esolangs.Cornucopia.ProgLoopSucc₂.wfDefs' : WFDefs' defs

@[simp]

instance Esolangs.Cornucopia.ProgLoopSucc₂.wf' : prog.WF'

@[simp]

theorem Esolangs.Cornucopia.ProgLoopSucc₂.compatibleDefs {n : ℕ} : CompatibleDefs (Map.ofList defs) (fs n)

@[simp]

theorem Esolangs.Cornucopia.ProgLoopSucc₂.compatible {n : ℕ} : prog.Compatible (builtinFs ∪ fs n)

@[simp]

theorem Esolangs.Cornucopia.ProgLoopSucc₂.builtin_not_mem_fs {n : ℕ} {b : Builtin} : b.name ∉ fs n

@[simp]

theorem Esolangs.Cornucopia.ProgLoopSucc₂.fs_eq_fs_iff {n m : ℕ} : fs n = fs m ↔ n = m

@[simp]

instance Esolangs.Cornucopia.ProgLoopSucc₂.wfWoutUnique_prog : prog.WFWoutUnique

@[instance_reducible]

instance Esolangs.Cornucopia.ProgLoopSucc₂.instProgInfoProg : ProgInfo prog

Equations

• Esolangs.Cornucopia.ProgLoopSucc₂.instProgInfoProg = { name := "LoopSucc₂", defNames := ["main"], has_model := true, has_unique_model := false, h_defNames := Esolangs.Cornucopia.ProgLoopSucc₂.instProgInfoProg._proof_1, h_wf' := Esolangs.Cornucopia.ProgLoopSucc₂.instProgInfoProg._proof_2, h_has_model := Esolangs.Cornucopia.ProgLoopSucc₂.instProgInfoProg._proof_3, h_has_unique_model := Esolangs.Cornucopia.ProgLoopSucc₂.instProgInfoProg._proof_4 }