Code corresponding to the PhD thesis of Yannick Forster

Computability in Constructive Type Theory

This is the Coq mechanisation of part I of "Computability in Constructive Type Theory", the PhD thesis of Yannick Forster.