Skip to content

Commit 14bbdf9

Browse files
committed
Updated README
1 parent 0ef1588 commit 14bbdf9

File tree

1 file changed

+27
-8
lines changed

1 file changed

+27
-8
lines changed

README.md

Lines changed: 27 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -15,17 +15,36 @@ Run `make .merlin` to create the `.merlin` file.
1515

1616
## New Vernacular Commands
1717

18-
A new vernacular command `CWTest msg? qualid Assumes qualid*` is defined.
19-
This command fails if the tested `qualid` depends on an axiom which is not listed
20-
after `Assumes`:
18+
- `CWTest string? qualid Assumes qualid*`
2119

22-
```coq
23-
CWTest "Testing lemma" lemma Assumes proof_irrelevance functional_extensionality.
24-
```
20+
This command fails if the tested `qualid` depends on an axiom which is not listed after `Assumes`:
21+
22+
```coq
23+
CWTest "Testing lemma" lemma Assumes proof_irrelevance functional_extensionality.
24+
```
25+
The string argument after `CWTest` is an optional message.
26+
27+
- `CWGroup string`
28+
29+
Begins a group of tests.
30+
31+
- `CWEndGroup`
32+
33+
Ends a group of tests.
34+
35+
- `CWFile string? Size < int`
36+
37+
Tests if the size of a file (the first string argument) is less than the second argument.
38+
39+
The file name is optional. The default file is the solution file.
40+
41+
- `CWFile string? Matches string`
42+
43+
Tests if the content of a file matches a regular expression (the second argument). The regular expression syntax is [OCaml Str](https://caml.inria.fr/pub/docs/manual-ocaml/libref/Str.html) (`\` should not be escaped).
2544

26-
The string argument after `CWTest` (`msg`) is optional.
45+
- `CWFile string? Does Not Match string`
2746

28-
Two other commands are `CWGroup msg` and `CWEndGroup`.
47+
Tests if the content of a file does not match a regular expression (the second argument).
2948

3049
## Examples
3150

0 commit comments

Comments
 (0)