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
53
54
55
56
57
58
59
60
61
62
63
|
From Tuto2 Require Import Loader.
(*** A no-op command ***)
Nothing.
(*** No-op commands with arguments ***)
(*
* Terminal parameters:
*)
Command With Some Terminal Parameters.
(* Command. *) (* does not parse *)
(*
* A single non-terminal argument:
*)
Pass 42.
(* Pass. *) (* does not parse *)
(* Pass True. *) (* does not parse *)
(* Pass 15 20. *) (* does not parse *)
(*
* A list of non-terminal arguments:
*)
Accept 100 200 300 400.
Accept.
Accept 2.
(*
* A custom argument:
*)
Foobar Foo.
Foobar Bar.
(*** Commands that give feedback ***)
(*
* Simple feedback:
*)
Is Everything Awesome.
(*** Storage and side effects ***)
(*
* Local side effects:
*)
Count.
Count.
Count.
(*
* See Count.v for behavior in modules that import this one.
*)
(*
* Persistent side effects:
*)
Count Persistent.
Count Persistent.
Count Persistent.
(*
* See Count.v for behavior in modules that import this one.
*)
|
