backup work for weekend

hazelgrove · Feb 7, 2025 · c22a807 · c22a807
1 parent dcfbbf7
commit c22a807
Show file tree

Hide file tree

Showing 7 changed files with 577 additions and 14 deletions.
diff --git a/src/haz3lcore/proof/Axioms.re b/src/haz3lcore/proof/Axioms.re
@@ -0,0 +1,41 @@
+let v: ProofCtx.t =
+  []
+  |> ProofCtx.add_entry(
+       "Iden(+)L",
+       Fun(
+         Var("x") |> Pat.fresh,
+         BinOp(
+           Int(Equals),
+           BinOp(Int(Plus), Var("x") |> Exp.fresh, Int(0) |> Exp.fresh)
+           |> Exp.fresh,
+           Var("x") |> Exp.fresh,
+         )
+         |> Exp.fresh,
+         Some(Int |> Typ.fresh),
+         None,
+       )
+       |> Exp.fresh,
+     )
+  |> ProofCtx.add_entry(
+       "Comm(+)",
+       Fun(
+         Var("x") |> Pat.fresh,
+         Fun(
+           Var("y") |> Pat.fresh,
+           BinOp(
+             Int(Equals),
+             BinOp(Int(Plus), Var("x") |> Exp.fresh, Var("y") |> Exp.fresh)
+             |> Exp.fresh,
+             BinOp(Int(Plus), Var("y") |> Exp.fresh, Var("x") |> Exp.fresh)
+             |> Exp.fresh,
+           )
+           |> Exp.fresh,
+           Some(Int |> Typ.fresh),
+           None,
+         )
+         |> Exp.fresh,
+         Some(Int |> Typ.fresh),
+         None,
+       )
+       |> Exp.fresh,
+     );