diff --git a/theories/F_mu_ref_conc/lang.v b/theories/F_mu_ref_conc/lang.v index 3fc614fa99565f9bf213bd07819900d72d281933..e78750bb44440c54a9020e6c00dca85bd824c86d 100644 --- a/theories/F_mu_ref_conc/lang.v +++ b/theories/F_mu_ref_conc/lang.v @@ -108,11 +108,11 @@ Module lang. | Mul, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a * b)) | Add, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a + b)) | Sub, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a - b)) - | Eq, LitV (Nat a), LitV (Nat b) => Some $ if decide (a = b) then LitV (Bool true) else LitV (Bool false) + | Eq, LitV (Nat a), LitV (Nat b) => Some $ LitV (Bool (if decide (a = b) then true else false)) | Eq, LitV (Bool a), LitV (Bool b) => Some $ LitV (Bool (eqb a b)) - | Eq, LitV (Loc l1), LitV (Loc l2) => Some $ if decide (l1 = l2) then LitV (Bool true) else LitV (Bool false) - | Le, LitV (Nat a), LitV (Nat b) => Some $ if le_dec a b then LitV (Bool true) else LitV (Bool false) - | Lt, LitV (Nat a), LitV (Nat b) => Some $ if lt_dec a b then LitV (Bool true) else LitV (Bool false) + | Eq, LitV (Loc l1), LitV (Loc l2) => Some $ LitV (Bool (if decide (l1 = l2) then true else false)) + | Le, LitV (Nat a), LitV (Nat b) => Some $ LitV (Bool (if le_dec a b then true else false)) + | Lt, LitV (Nat a), LitV (Nat b) => Some $ LitV (Bool (if lt_dec a b then true else false)) | Xor, LitV (Bool a), LitV (Bool b) => Some $ LitV (Bool (xorb a b)) | _,_,_ => None end.