<commit_before># A formalization of type theory in Coq

This Coq library formalizes dependent type theory in the style of Per Martin-Löf. The
formalization is *configurable* in the sense that various components can be turned on or
off, or be left ambivalent. It is thus easy to instantiate many variants of type theory,
such as extensional vs. intensional, with or without universes, etc. The library also
formalizes several meta-theorems about type theory.

## Requirements

### Requirements for compiling the library

The library works with Coq 8.6, and probably with many other recent versions as well, as
it does not use any special features of Coq. You may find out about the best way to install Coq at the [Coq web site](If you do not have Coq, visit).

To compile the library you need Coq and [`make`](https://www.gnu.org/software/make/).

### Requirements for generating the LaTeX version of rules

In order to generate the LaTeX version of the rules you
need [Python](https://www.python.org) (either version 2.7 or 3.x) and (obviously) LaTeX,
as well as the [mathpartir](http://cristal.inria.fr/~remy/latex/) package<commit_msg>Add Coq website address to README<commit_after># A formalization of type theory in Coq

This Coq library formalizes dependent type theory in the style of Per Martin-Löf. The
formalization is *configurable* in the sense that various components can be turned on or
off, or be left ambivalent. It is thus easy to instantiate many variants of type theory,
such as extensional vs. intensional, with or without universes, etc. The library also
formalizes several meta-theorems about type theory.

## Requirements

### Requirements for compiling the library

The library works with Coq 8.6, and probably with many other recent versions as well, as
it does not use any special features of Coq. You may find out about the best way to install Coq at the [Coq web site](https://coq.inria.fr/).

To compile the library you need Coq and [`make`](https://www.gnu.org/software/make/).

### Requirements for generating the LaTeX version of rules

In order to generate the LaTeX version of the rules you
need [Python](https://www.python.org) (either version 2.7 or 3.x) and (obviously) LaTeX,
as well as the [mathpartir](http://cristal.inria.fr/~remy/latex/) package
{'fraction_non_alphanumeric': 0.07130358705161854, 'fraction_numerical': 0.004374453193350831, 'mean_word_length': 4.432304038004751, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 5, 'lorem ipsum': 0, 'www.': 4, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1104995', 'n_tokens_mistral': 665, 'n_tokens_neox': 626, 'n_words': 334}