Overview

== Formalization of normalization-by-evaluation for Martin Lof Type Theory with Universe.
== Pawel Wieczorek, University of Wroclaw, Poland


>>> Introduction

This package contains formalization of NBE for dependend type thoery in Martin-Lof style. Main goal of this
project is to provide certified normalizer and decision procedure for term/type equality.

Second goal is to provide well-written package, which could be easy modifiable by other people.

Package is written for Coq 8.4pl3 (February 2014).

>>> Type Theory