Commit 679d06d1 by Robbert Krebbers

### Simplify Texan triple notations.

parent c1120a90
 ... @@ -51,26 +51,24 @@ Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q)) ... @@ -51,26 +51,24 @@ Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q)) format "'WP' e {{ v , Q } }") : uPred_scope. format "'WP' e {{ v , Q } }") : uPred_scope. (* Texan triples *) (* Texan triples *) Notation "'{{{' pre } } } e {{{ x .. y ; pat , post } } }" := Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" := (∀ (ψ : _ → uPred _), (∀ Φ : _ → uPred _, (pre ★ ▷ (∀ x, .. (∀ y, post -★ ψ (pat)%V) .. )%I) ⊢ WP e {{ ψ }}) P ★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) ⊢ WP e {{ Φ }}) (at level 20, x closed binder, y closed binder, (at level 20, x closed binder, y closed binder, format "{{{ pre } } } e {{{ x .. y ; pat , post } } }") : C_scope. format "{{{ P } } } e {{{ x .. y ; pat , Q } } }") : C_scope. Notation "'{{{' pre } } } e @ E {{{ x .. y ; pat , post } } }" := Notation "'{{{' P } } } e @ E {{{ x .. y ; pat , Q } } }" := (∀ (ψ : _ → uPred _), (∀ Φ : _ → uPred _, (pre ★ ▷ (∀ x, .. (∀ y, post -★ ψ (pat)%V) .. )%I) ⊢ WP e @ E {{ ψ }}) P ★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) ⊢ WP e @ E {{ Φ }}) (at level 20, x closed binder, y closed binder, (at level 20, x closed binder, y closed binder, format "{{{ pre } } } e @ E {{{ x .. y ; pat , post } } }") : C_scope. format "{{{ P } } } e @ E {{{ x .. y ; pat , Q } } }") : C_scope. Notation "'{{{' pre } } } e {{{ ; pat , post } } }" := Notation "'{{{' P } } } e {{{ ; pat , Q } } }" := (∀ (ψ : _ → uPred _), (∀ Φ : _ → uPred _, P ★ ▷ (Q -★ Φ pat%V) ⊢ WP e {{ Φ }}) (pre ★ ▷ (post -★ ψ (pat)%V)%I) ⊢ WP e {{ ψ }}) (at level 20, (at level 20, format "{{{ pre } } } e {{{ ; pat , post } } }") : C_scope. format "{{{ P } } } e {{{ ; pat , Q } } }") : C_scope. Notation "'{{{' pre } } } e @ E {{{ ; pat , post } } }" := Notation "'{{{' P } } } e @ E {{{ ; pat , Q } } }" := (∀ (ψ : _ → uPred _), (∀ Φ : _ → uPred _, P ★ ▷ (Q -★ Φ pat%V) ⊢ WP e @ E {{ Φ }}) (pre ★ ▷ (post -★ ψ (pat)%V)%I) ⊢ WP e @ E {{ ψ }}) (at level 20, (at level 20, format "{{{ pre } } } e @ E {{{ ; pat , post } } }") : C_scope. format "{{{ P } } } e @ E {{{ ; pat , Q } } }") : C_scope. Section wp. Section wp. Context `{irisG Λ Σ}. Context `{irisG Λ Σ}. ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!