Commit 2023-06-29 18:49 b2f1e713

View on Github →

feat: port Archive.Arithcc (#5595)

Estimated changes

Modified Archive.lean

Created Archive/Arithcc.lean

added inductive Arithcc.Expr

added def Arithcc.Identifier

added inductive Arithcc.Instruction

added theorem Arithcc.Register.le_of_lt_succ

added theorem Arithcc.Register.lt_succ_self

added def Arithcc.Register

added structure Arithcc.State

added def Arithcc.StateEq

added def Arithcc.StateEqRs

added def Arithcc.Word

added def Arithcc.compile

added theorem Arithcc.compiler_correctness

added def Arithcc.loc

added def Arithcc.outcome

added theorem Arithcc.outcome_append

added def Arithcc.read

added theorem Arithcc.stateEqRs_implies_write_eq_rs

added theorem Arithcc.stateEq_implies_write_eq

added def Arithcc.step

added def Arithcc.value

added def Arithcc.write

added theorem Arithcc.write_eq_implies_stateEq