Commit 327ba441 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix priorities of IntoLaterN instances.

This should fix iris-examples.
parent 688de435
Pipeline #6306 passed with stages
in 10 minutes and 5 seconds
......@@ -168,19 +168,19 @@ Proof. by rewrite /FromAlways. Qed.
(* IntoLater *)
Global Instance into_laterN_later n P Q :
IntoLaterN n P Q IntoLaterN' (S n) ( P) Q.
IntoLaterN n P Q IntoLaterN' (S n) ( P) Q | 0.
Proof. by rewrite /IntoLaterN' /IntoLaterN =>->. Qed.
Global Instance into_laterN_later_further n P Q :
IntoLaterN' n P Q IntoLaterN' n ( P) ( Q).
IntoLaterN' n P Q IntoLaterN' n ( P) ( Q) | 1000.
Proof. rewrite /IntoLaterN' /IntoLaterN =>->. by rewrite -laterN_later. Qed.
Global Instance into_laterN_laterN n P : IntoLaterN' n (^n P) P.
Global Instance into_laterN_laterN n P : IntoLaterN' n (^n P) P | 0.
Proof. done. Qed.
Global Instance into_laterN_laterN_plus n m P Q :
IntoLaterN m P Q IntoLaterN' (n + m) (^n P) Q.
IntoLaterN m P Q IntoLaterN' (n + m) (^n P) Q | 1.
Proof. rewrite /IntoLaterN' /IntoLaterN=>->. by rewrite laterN_plus. Qed.
Global Instance into_laterN_laterN_further n m P Q :
IntoLaterN' m P Q IntoLaterN' m (^n P) (^n Q).
IntoLaterN' m P Q IntoLaterN' m (^n P) (^n Q) | 1000.
Proof.
rewrite /IntoLaterN' /IntoLaterN=>->. by rewrite -!laterN_plus Nat.add_comm.
Qed.
......
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