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

mono_nat_update: make first argument implicit

parent e23bc97f
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris/algebra/lib/mono_nat.v
+ 1
− 1
View file @ 93c00401
......@@ -79,7 +79,7 @@ Section mono_nat.
Lemma mono_nat_included q n : mono_nat_lb n ≼ mono_nat_auth q n.
Proof. apply cmra_included_r. Qed.
Lemma mono_nat_update n n' :
Lemma mono_nat_update {n} n' :
n ≤ n' →
mono_nat_auth 1 n ~~> mono_nat_auth 1 n'.
Proof.
......
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