6 lines
371 B
Markdown
6 lines
371 B
Markdown
# An algorithm for type-checking dependent types
|
|
|
|
A "modern" implementation of algorithm described in Thierry Coquand's paper. This employs some monad nicities compared to the haskell implementation in the paper (and isn't a pdf).
|
|
|
|
This isn't meant to be "better", it might even be more confusing to you. I wrote this to get more of a feel for checking dependent types.
|