proposition: Lemma CompileBinopOrTest: forall {av} name var1 var2 (val1 val2: W) ext op (tenv: Telescope av), name ∉ ext -> NotInTelescope name tenv -> StringMap.MapsTo var1 (wrap val1) ext -> StringMap.MapsTo var2 (wrap val2) ext -> forall env, {{ tenv }} Assign name (WrapOpInExpr op (Var var1) (Var var2)) {{ [[`name ->> (eval_binop op val1 val2) as _]]::tenv }} ∪ {{ ext }} // env.
proof: Proof. destruct op; SameValues_Facade_t. Qed.
imports: CertifiedExtraction.Extraction.Core CertifiedExtraction.Extraction.Basics