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

Equations

• Esolangs.Cornucopia.ProgId.defs = [(Esolangs.Cornucopia.mainName, Esolangs.Cornucopia.defId)]

def Esolangs.Cornucopia.ProgId.fs : Map String (List ℕ → ℕ)

Equations

• Esolangs.Cornucopia.ProgId.fs = Map.ofList [(Esolangs.Cornucopia.mainName, Esolangs.Cornucopia.fn 1 fun (x : List ℕ) => x[0]!)]

def Esolangs.Cornucopia.ProgId.prog : Prog

Equations

• Esolangs.Cornucopia.ProgId.prog = Esolangs.Cornucopia.Prog.ofDefs Esolangs.Cornucopia.ProgId.defs

@[simp]

theorem Esolangs.Cornucopia.ProgId.nodup_prog : (List.map (fun (x : String × Def) => x.1) defs).Nodup

@[simp]

theorem Esolangs.Cornucopia.ProgId.wfDefs' : WFDefs' defs

@[simp]

instance Esolangs.Cornucopia.ProgId.wf' : prog.WF'

@[simp]

theorem Esolangs.Cornucopia.ProgId.compatibleDefs : CompatibleDefs (Map.ofList defs) fs

@[simp]

theorem Esolangs.Cornucopia.ProgId.compatible : prog.Compatible (builtinFs ∪ fs)

@[simp]

instance Esolangs.Cornucopia.ProgId.wf_prog : prog.WF

@[simp]

theorem Esolangs.Cornucopia.ProgId.fs_prog : prog.fs = builtinFs ∪ fs

@[simp]

theorem Esolangs.Cornucopia.ProgId.run_prog {n : ℕ} : prog.run n = n

@[instance_reducible]

instance Esolangs.Cornucopia.ProgId.instProgInfoProg : ProgInfo prog

Equations

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