Yannick Forster [email protected]
This is the Coq mechanisation of the paper "Church’s thesis and related axioms in Coq’s type theory ".
You need The Coq Proof Assistant, version 8.11.0 and the stdpp library installed
Afterwards, you can type make in the coq directory.