Skip to content
Snippets Groups Projects
Commit 9333e8d2 authored by Ralf Jung's avatar Ralf Jung
Browse files

use lia instead of omega

parent d19b7d23
Branches
No related tags found
No related merge requests found
Pipeline #33598 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
theories/typing/lib/rwlock/rwlock_code.v
+ 1
− 1
View file @ 9333e8d2
...@@ -246,7 +246,7 @@ Section rwlock_functions. ...@@ -246,7 +246,7 @@ Section rwlock_functions.
iDestruct (monPred_objectively_elim with "Hβtok2") as "Hβtok2". iDestruct (monPred_objectively_elim with "Hβtok2") as "Hβtok2".
iModIntro. iModIntro.
destruct st2 as [[[]|[[ν q] n]]|]; simpl in Eqst2. destruct st2 as [[[]|[[ν q] n]]|]; simpl in Eqst2.
- exfalso. clear -Eqst2 Hm1. rewrite Eqst2 in Hm1. omega. - exfalso. clear -Eqst2 Hm1. rewrite Eqst2 in Hm1. lia.
- rewrite Eqst2. iDestruct "INT" as "[$ INT]". - rewrite Eqst2. iDestruct "INT" as "[$ INT]".
iExists (). iSplitL ""; [done|]. iIntros (t2 Ext2) "W' !>". iSplitL "". iExists (). iSplitL ""; [done|]. iIntros (t2 Ext2) "W' !>". iSplitL "".
{ rewrite /Q1 Eqst2. by iIntros "!> $". } iIntros "!> !>". { rewrite /Q1 Eqst2. by iIntros "!> $". } iIntros "!> !>".
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment