Commit 7709aeaf authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Non-primitive VS that take a step.

parent 3ef40c00
......@@ -12,6 +12,13 @@ Notation "P ={ E }=> Q" := (P ={E,E}=> Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=> Q") : uPred_scope.
Notation "P ={ E1 , E2 }▷=> Q" := (P ={E1%I,E2%I}=> |={E2,E1}=> Q)%I
(at level 99, E1, E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }▷=> Q") : uPred_scope.
Notation "P ={ E }▷=> Q" := (P ={E,E}=> Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ={ E }▷=> Q") : uPred_scope.
Section vs.
Context `{irisG Λ Σ}.
Implicit Types P Q R : iProp Σ.
......
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