Source code as when published as a CDMTCS research report

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

Source code as at dissertation submission time

Source code as at submission time on 27 February 2018, for 'Formalising Martin-Löf's Theorem Using Coq', an honours dissertation at the University of Auckland.

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