Commit bbdc4d66 authored by Gregory Malecha's avatar Gregory Malecha

CHANGE <intuit> to <#>

parent 803e091e
......@@ -156,7 +156,7 @@ s/\blist_singletonM_included\b/list_singleton_included/g
- quantifiers[†]: `forall` for `∀` and `exists` for `∃`
- separation logic: `**` for `∗`, `-*` for `-∗`, and `*-*` for `∗-∗`
- step indexing: `|>` for `▷`
- modalities: `<intuit>` for `□` and `<except_0>` for `◇`
- modalities: `<#>` for `□` and `<except_0>` for `◇`
- most derived notations can be computed from previous notations using the
substitutions above, e.g. replace `∗` with `*` and `▷` with `|>`. Examples
include the following:
......
......@@ -11,10 +11,10 @@ Section base_logic_tests.
Lemma test_random_stuff (P1 P2 P3 : nat -> uPred M) :
|-- forall (x y : nat) a b,
x y ->
<intuit> (uPred_ownM (a b) -*
(exists y1 y2 c, P1 ((x + y1) + y2) True <intuit> uPred_ownM c) -*
<intuit> |> (forall z, P2 z True -> P2 z) -*
|> (forall n m : nat, P1 n -> <intuit> (True P2 n -> <intuit> (n = n P3 n))) -*
<#> (uPred_ownM (a b) -*
(exists y1 y2 c, P1 ((x + y1) + y2) True <#> uPred_ownM c) -*
<#> |> (forall z, P2 z True -> P2 z) -*
|> (forall n m : nat, P1 n -> <#> (True P2 n -> <#> (n = n P3 n))) -*
|> x = 0 \/ exists x z, |> P3 (x + z) ** uPred_ownM b ** uPred_ownM (core b)).
Proof.
iIntros (i [|j] a b ?) "!> [Ha Hb] H1 #H2 H3"; setoid_subst.
......
......@@ -50,8 +50,8 @@ Notation "P <-> Q" := (P ↔ Q)%I (at level 95, no associativity, only parsing)
Notation "P *-* Q" := (P - Q)%I (at level 95, no associativity, only parsing) : bi_scope.
Notation "'<intuit>' P" := ( P)%I (at level 20, right associativity, only parsing) : bi_scope.
Notation "'<intuit>?' p P" := (?p P)%I (at level 20, p at level 9, P at level 20,
Notation "'<#>' P" := ( P)%I (at level 20, right associativity, only parsing) : bi_scope.
Notation "'<#>?' p P" := (?p P)%I (at level 20, p at level 9, P at level 20,
right associativity, only parsing) : bi_scope.
Notation "'<except_0>' P" := ( P)%I (at level 20, right associativity, only parsing) : bi_scope.
......
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