/infinitary-rewriting-coq

Infinitary Rewriting in Coq
  1. Coq 98.5%
  2. Shell 1.5%
Switch branches/tags
Nothing to show
Find file
Clone or download

Clone with HTTPS

Use Git or checkout with SVN using the web URL.

Download ZIP

Launching GitHub Desktop...

If nothing happens, download GitHub Desktop and try again.

Launching GitHub Desktop...

If nothing happens, download GitHub Desktop and try again.

Launching Xcode...

If nothing happens, download Xcode and try again.

Launching Visual Studio...

If nothing happens, download the GitHub extension for Visual Studio and try again.

Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
web
Context.v
ContextEquality.v
ExampleABA.v
FiniteTerm.v
LICENSE
Makefile
NoUniqueNormalFormsWO.v
NoUniqueNormalFormsWOElaborated.v
Ordinal.v
Prelims.v
README
Rewriting.v
Signature.v
Substitution.v
Term.v
TermEquality.v
Variables.v
Vector.v
WfOrdinal.v
get-related

README 

Infinitary Rewriting in Coq

Copyright (c) 2010, Martijn Vermaat <martijn@vermaat.name>
                    Dimitri Hendriks <diem@cs.vu.nl>

Licensed under the MIT license, see the LICENSE file or

  http://en.wikipedia.org/wiki/Mit_license


For documentation, see

  Martijn Vermaat.
  Infinitary Rewriting in Coq.
  Master Thesis, VU University Amsterdam, 2010.

  http://martijn.vermaat.name/master-project


Compile by typing

  make

and generate a new Makefile by typing

  coq_makefile -no-install -I . *.v -o Makefile

HTML Coqdoc files can be generated by

  coqdoc --html --toc --coqlib http://coq.inria.fr/stdlib/ -d web/coqdoc *.v