blob: edd5c8d73d812f8f4ea5e82464a48e8173224105 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
(* Supporting imp. params. in inductive or fixpoints mutually defined with a notation *)
Reserved Notation "* a" (at level 70).
Inductive P {n : nat} : nat -> Prop :=
| c m : *m
where "* m" := (P m).
Reserved Notation "##".
Inductive I {A:Type} := C : ## where "##" := I.
(* The following was working in 8.6 *)
Require Import Vector.
Reserved Notation "# a" (at level 70).
Fixpoint f {n : nat} (v:Vector.t nat n) : nat :=
match v with
| nil _ => 0
| cons _ _ _ v => S (#v)
end
where "# v" := (f v).
(* The following was working in 8.6 *)
Reserved Notation "%% a" (at level 70).
Record R :=
{g : forall {A} (a:A), a=a where "%% x" := (g x);
k : %% 0 = eq_refl}.
|