Skip to content
Snippets Groups Projects
Commit fcfe7652 authored by Ralf Jung's avatar Ralf Jung Committed by Ike Mulder
Browse files

Explicitly mention DfracDiscarded in match.

parent 28597c57
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris/base_logic/algebra.v
+ 1
− 1
View file @ fcfe7652
...@@ -30,7 +30,7 @@ Section upred. ...@@ -30,7 +30,7 @@ Section upred.
✓ dq ⊣⊢ match dq with ✓ dq ⊣⊢ match dq with
| DfracOwn q => ⌜q ≤ 1⌝%Qp | DfracOwn q => ⌜q ≤ 1⌝%Qp
| DfracBoth q => ⌜q < 1⌝%Qp | DfracBoth q => ⌜q < 1⌝%Qp
| _ => True | DfracDiscarded => True
end. end.
Proof. destruct dq; by rewrite uPred.discrete_valid. Qed. Proof. destruct dq; by rewrite uPred.discrete_valid. Qed.
......
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