blob: a6ebda61cfd90a303257aea3dcd4000029aeba13 (
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
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
|
(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*)
Require Import Coq.Lists.List.
Require Import Coq.Vectors.Vector.
Import ListNotations.
Import VectorNotations.
Set Implicit Arguments.
Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T).
Arguments mynil {_}, _.
Delimit Scope mylist_scope with mylist.
Bind Scope mylist_scope with mylist.
Delimit Scope vector_scope with vector.
Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
Notation " [ x ] " := (mycons x mynil) : mylist_scope.
Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope.
(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4. There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *)
Check [ ]%mylist : mylist _.
Check [ ]%list : list _.
Check []%vector : Vector.t _ _.
Check [ _ ]%mylist : mylist _.
Check [ _ ]%list : list _.
Check [ _ ]%vector : Vector.t _ _.
Check [ _ ; _ ]%list : list _.
Check [ _ ; _ ]%vector : Vector.t _ _.
Check [ _ ; _ ]%mylist : mylist _.
Check [ _ ; _ ; _ ]%list : list _.
Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
Check [ _ ; _ ; _ ]%mylist : mylist _.
Check [ _ ; _ ; _ ; _ ]%list : list _.
Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope.
(* Now these all work, but not so in 8.4. If we get the ability to remove notations, this section can also just be removed. *)
Check [ ]%mylist : mylist _.
Check [ ]%list : list _.
Check []%vector : Vector.t _ _.
Check [ _ ]%mylist : mylist _.
Check [ _ ]%list : list _.
Check [ _ ]%vector : Vector.t _ _.
Check [ _ ; _ ]%list : list _.
Check [ _ ; _ ]%vector : Vector.t _ _.
Check [ _ ; _ ]%mylist : mylist _.
Check [ _ ; _ ; _ ]%list : list _.
Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
Check [ _ ; _ ; _ ]%mylist : mylist _.
Check [ _ ; _ ; _ ; _ ]%list : list _.
Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
|
