Post's Theorem in Coq

This repository contains the Coq mechanization of "The Arithmetical Hierarchy, Oracle Computability, and Post's Theorem in Synthetic Computability", the Bachelor's thesis of Niklas Mück.

How to compile

Install coq=8.15.2 and coq-equations=1.3+8.15 then run $ make

External files

All files in the external/ folder are external.

• FOL/, Shared/, and Synthetic/ are taken from the upcoming Coq Library for Mechanised First-Order Logic.
• partial.v and mu_nat.v are taken from the Coq mechanization of the PhD thesis of Yannick Forster.

To reduce dependencies, some imports are changed and some code is commented out or removed.