Commit b65cf679 authored by Ralf Jung's avatar Ralf Jung

fix format spacing for texan triples

parent 10c61064
Pipeline #9622 passed with stage
in 27 minutes and 7 seconds
......@@ -89,93 +89,93 @@ Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ s; E {{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "{{{ P } } } e @ s ; E {{{ x .. y , RET pat ; Q } } }") : bi_scope.
format "{{{ P } } } e @ s ; E {{{ x .. y , RET pat ; Q } } }") : bi_scope.
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E {{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "{{{ P } } } e @ E {{{ x .. y , RET pat ; Q } } }") : bi_scope.
format "{{{ P } } } e @ E {{{ x .. y , RET pat ; Q } } }") : bi_scope.
Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E ?{{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "{{{ P } } } e @ E ? {{{ x .. y , RET pat ; Q } } }") : bi_scope.
format "{{{ P } } } e @ E ? {{{ x .. y , RET pat ; Q } } }") : bi_scope.
Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e {{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "{{{ P } } } e {{{ x .. y , RET pat ; Q } } }") : bi_scope.
format "{{{ P } } } e {{{ x .. y , RET pat ; Q } } }") : bi_scope.
Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e ?{{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "{{{ P } } } e ? {{{ x .. y , RET pat ; Q } } }") : bi_scope.
format "{{{ P } } } e ? {{{ x .. y , RET pat ; Q } } }") : bi_scope.
Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
( Φ, P - (Q - Φ pat%V) - WP e @ s; E {{ Φ }})%I
(at level 20,
format "{{{ P } } } e @ s ; E {{{ RET pat ; Q } } }") : bi_scope.
format "{{{ P } } } e @ s ; E {{{ RET pat ; Q } } }") : bi_scope.
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
( Φ, P - (Q - Φ pat%V) - WP e @ E {{ Φ }})%I
(at level 20,
format "{{{ P } } } e @ E {{{ RET pat ; Q } } }") : bi_scope.
format "{{{ P } } } e @ E {{{ RET pat ; Q } } }") : bi_scope.
Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
( Φ, P - (Q - Φ pat%V) - WP e @ E ?{{ Φ }})%I
(at level 20,
format "{{{ P } } } e @ E ? {{{ RET pat ; Q } } }") : bi_scope.
format "{{{ P } } } e @ E ? {{{ RET pat ; Q } } }") : bi_scope.
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
( Φ, P - (Q - Φ pat%V) - WP e {{ Φ }})%I
(at level 20,
format "{{{ P } } } e {{{ RET pat ; Q } } }") : bi_scope.
format "{{{ P } } } e {{{ RET pat ; Q } } }") : bi_scope.
Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
( Φ, P - (Q - Φ pat%V) - WP e ?{{ Φ }})%I
(at level 20,
format "{{{ P } } } e ? {{{ RET pat ; Q } } }") : bi_scope.
format "{{{ P } } } e ? {{{ RET pat ; Q } } }") : bi_scope.
Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ : _ uPred _,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ s; E {{ Φ }})
(at level 20, x closed binder, y closed binder,
format "{{{ P } } } e @ s ; E {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
format "{{{ P } } } e @ s ; E {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ : _ uPred _,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E {{ Φ }})
(at level 20, x closed binder, y closed binder,
format "{{{ P } } } e @ E {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
format "{{{ P } } } e @ E {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ : _ uPred _,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E ?{{ Φ }})
(at level 20, x closed binder, y closed binder,
format "{{{ P } } } e @ E ? {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
format "{{{ P } } } e @ E ? {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ : _ uPred _,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e {{ Φ }})
(at level 20, x closed binder, y closed binder,
format "{{{ P } } } e {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
format "{{{ P } } } e {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ : _ uPred _,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e ?{{ Φ }})
(at level 20, x closed binder, y closed binder,
format "{{{ P } } } e ? {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
format "{{{ P } } } e ? {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
( Φ : _ uPred _, P - (Q - Φ pat%V) - WP e @ s; E {{ Φ }})
(at level 20,
format "{{{ P } } } e @ s ; E {{{ RET pat ; Q } } }") : stdpp_scope.
format "{{{ P } } } e @ s ; E {{{ RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
( Φ : _ uPred _, P - (Q - Φ pat%V) - WP e @ E {{ Φ }})
(at level 20,
format "{{{ P } } } e @ E {{{ RET pat ; Q } } }") : stdpp_scope.
format "{{{ P } } } e @ E {{{ RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
( Φ : _ uPred _, P - (Q - Φ pat%V) - WP e @ E ?{{ Φ }})
(at level 20,
format "{{{ P } } } e @ E ? {{{ RET pat ; Q } } }") : stdpp_scope.
format "{{{ P } } } e @ E ? {{{ RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
( Φ : _ uPred _, P - (Q - Φ pat%V) - WP e {{ Φ }})
(at level 20,
format "{{{ P } } } e {{{ RET pat ; Q } } }") : stdpp_scope.
format "{{{ P } } } e {{{ RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
( Φ : _ uPred _, P - (Q - Φ pat%V) - WP e ?{{ Φ }})
(at level 20,
format "{{{ P } } } e ? {{{ RET pat ; Q } } }") : stdpp_scope.
format "{{{ P } } } e ? {{{ RET pat ; Q } } }") : stdpp_scope.
Section wp.
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!
Please register or to comment