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

Equations

• Esolangs.Cornucopia.ProgLoopSucc₁.defs = [(Esolangs.Cornucopia.mainName, Esolangs.Cornucopia.defLoopSucc₁ Esolangs.Cornucopia.mainName)]

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]

instance Esolangs.Cornucopia.ProgLoopSucc₁.wfWoutModel_prog : prog.WFWoutModel

@[instance_reducible]

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

Equations

• Esolangs.Cornucopia.ProgLoopSucc₁.instProgInfoProg = { name := "LoopSucc₁", defNames := ["main"], has_model := false, 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 }