Commit 5d3fe67e authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files


parent 3b2f7704
......@@ -349,7 +349,7 @@ Proof.
refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
Instance expr_inhabited : Inhabited (expr) := populate (Lit LitUnit).
Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit).
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
Canonical Structure stateC := leibnizC state.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment