Commit 41400739 authored by Ralf Jung's avatar Ralf Jung
Browse files

exhaustive match for lit_is_unboxed

parent 3a3f0706
Pipeline #28341 passed with stage
in 15 minutes and 32 seconds
......@@ -162,7 +162,7 @@ Definition lit_is_unboxed (l: base_lit) : Prop :=
(** Disallow comparing (erased) prophecies with (erased) prophecies, by
considering them boxed. *)
| LitProphecy _ | LitPoison => False
| _ => True
| LitInt _ | LitBool _ | LitLoc _ | LitUnit => True
end.
Definition val_is_unboxed (v : val) : Prop :=
match v with
......
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