Skip to content

Commit

Permalink
Merge branch 'artifact' of github.com:zhezhouzz/HATs into artifact
Browse files Browse the repository at this point in the history
  • Loading branch information
zhezhouzz committed Mar 11, 2024
2 parents 570797c + 8408c84 commit fec3036
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -199,7 +199,7 @@ The following command performs the basic type check (and normalization which con

$ ./_build/default/bin/main.exe ri-ntype-check meta-config.json data/ri/FileSystem_Tree/init.ml

By enable the `preprocess` option in the config file `meta-config.json`, **Marple** will print the result of preprocess: desugaring, basic type check, and normalization. The details can be found in [Configuration of Marple](#configuration-of-marple).
By enabling the `preprocess` option in the config file `meta-config.json`, **Marple** will print the result of preprocess: desugaring, basic type check, and normalization. The details can be found in [Configuration of Marple](#configuration-of-marple).

**Requirements:** We use bold and colored printing in the command line, make sure your terminal supports escape sequences.

Expand Down
2 changes: 1 addition & 1 deletion formalization/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ opam pin coq-stdpp 1.9.0
opam pin coq-hammer-tactics 1.3.2+8.18
```

> Notice: We have installed all dependencies lised above in our docker image.
> Notice: We have installed all dependencies listed above in our docker image.
To build and check the Coq formalization, simply run `make` in the
`formalization` directory. The command `Print Assumptions soundness` at the end
Expand Down

0 comments on commit fec3036

Please sign in to comment.