Vermillion

LL(1) parser generator verified in Coq

This project has been tested with Coq version 8.8.1.

To build the project:

make

To delete generated files:

make clean

Main.v contains the main correctness theorems:

Example.v contains a tutorial on how to use the tool.

Name		Name	Last commit message	Last commit date
Latest commit History 291 Commits
Evaluation		Evaluation
Proofs		Proofs
.gitignore		.gitignore
Example.v		Example.v
Generator.v		Generator.v
Grammar.v		Grammar.v
LICENSE		LICENSE
Lemmas.v		Lemmas.v
Main.v		Main.v
Makefile		Makefile
NoDupDec.v		NoDupDec.v
Parser.v		Parser.v
README.md		README.md
Tactics.v		Tactics.v
Utils.v		Utils.v
_CoqProject		_CoqProject