Source code for 'Formalising Martin-Löf's Theorem Using Coq', an honours dissertation at the University of Auckland published as a Centre for Discrete Mathematics and Theoretical Computer Science research report (https://www.cs.auckland.ac.nz/research/groups/CDMTCS/researchreports/index.php?download&paper_file=679).
By Daniel Britten - supervised by Cristian S. Calude - and with guidance from Monica Marcus.
In order to interactively step through the proofs in this dissertation, please download CoqIde from https://coq.inria.fr/download or https://github.com/coq/coq/releases/tag/V8.7.2
To view the latest version of this project, see https://github.com/Coda-Coda/MartinLoefTheorem-Dissertation