Commit 1fb156c3 by Robbert Krebbers

### Fix levels of step-indexd in validN and includedN.

```This fix removes superflous white space in pretty printing. For example
✓{S n} x was pretty printed incorrectly as ✓{(S n)} x.```
parent 358b3e1d
 ... @@ -21,7 +21,7 @@ Infix "⩪" := minus (at level 40) : C_scope. ... @@ -21,7 +21,7 @@ Infix "⩪" := minus (at level 40) : C_scope. Class ValidN (A : Type) := validN : nat → A → Prop. Class ValidN (A : Type) := validN : nat → A → Prop. Instance: Params (@validN) 3. Instance: Params (@validN) 3. Notation "✓{ n } x" := (validN n x) Notation "✓{ n } x" := (validN n x) (at level 20, n at level 1, format "✓{ n } x"). (at level 20, n at next level, format "✓{ n } x"). Class Valid (A : Type) := valid : A → Prop. Class Valid (A : Type) := valid : A → Prop. Instance: Params (@valid) 2. Instance: Params (@valid) 2. ... @@ -30,7 +30,7 @@ Instance validN_valid `{ValidN A} : Valid A := λ x, ∀ n, ✓{n} x. ... @@ -30,7 +30,7 @@ Instance validN_valid `{ValidN A} : Valid A := λ x, ∀ n, ✓{n} x. Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x ⋅ z. Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x ⋅ z. Notation "x ≼{ n } y" := (includedN n x y) Notation "x ≼{ n } y" := (includedN n x y) (at level 70, format "x ≼{ n } y") : C_scope. (at level 70, n at next level, format "x ≼{ n } y") : C_scope. Instance: Params (@includedN) 4. Instance: Params (@includedN) 4. Hint Extern 0 (_ ≼{_} _) => reflexivity. Hint Extern 0 (_ ≼{_} _) => reflexivity. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!