diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v index d316826c67c643904b6708e3e01b75a63a63b84d..45f540eceb521c8268ac27054fa2720bbb402d86 100644 --- a/theories/heap_lang/lang.v +++ b/theories/heap_lang/lang.v @@ -317,6 +317,7 @@ Definition subst' (mx : binder) (es : expr) : expr → expr := Definition un_op_eval (op : un_op) (v : val) : option val := match op, v with | NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b) + | NegOp, LitV (LitInt n) => Some $ LitV $ LitInt (Z.lnot n) | MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n) | _, _ => None end.