Commit cb27aa7f authored by Ralf Jung's avatar Ralf Jung

use decide instead of bool_decide where possible

parent 1889960b
......@@ -520,7 +520,7 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
if decide (op = EqOp) then
(* Crucially, this compares the same way as [CmpXchg]! *)
if bool_decide (vals_compare_safe v1 v2) then
if decide (vals_compare_safe v1 v2) then
Some $ LitV $ LitBool $ bool_decide (v1 = v2)
else
None
......
......@@ -172,7 +172,7 @@ Proof.
intros Hcompare.
cut (bin_op_eval EqOp v1 v2 = Some $ LitV $ LitBool $ bool_decide (v1 = v2)).
{ intros. revert Hcompare. solve_pure_exec. }
rewrite /bin_op_eval /= bool_decide_true //.
rewrite /bin_op_eval /= decide_True //.
Qed.
Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
......
Markdown is supported
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