Commit f0f8f422 authored by David Swasey's avatar David Swasey

Typos in (unused) notation.

parent fcbf8d58
......@@ -153,9 +153,9 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
Notation "p → q" := (BI.impl p q : Props) (at level 55, right associativity) : iris_scope.
Notation "p '-*' q" := (si p q : Props) (at level 55, right associativity) : iris_scope.
Notation "∀ x , p" := (all n[(fun x => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
Notation "∃ x , p" := (all n[(fun x => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
Notation "∃ x , p" := (xist n[(fun x => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
Notation "∀ x : T , p" := (all n[(fun x : T => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
Notation "∃ x : T , p" := (all n[(fun x : T => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
Notation "∃ x : T , p" := (xist n[(fun x : T => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
Lemma valid_iff p :
valid p <-> ( p).
......
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