This document gives an explanation of src/lib/check.ml. This file implements a type check for our
dependent type theory. For an explanation of the type theory in general, please see either test/
or nbe-explanation.md.
This explanation has not yet been completed. In the mean time I refer the curious to
"A simple type-theoretic language: Mini-TT" by Thierry Coquand, Yoshiki Kinoshita, Bengt Nordström, and Makoto Takeyama.