GitHub - huevosybacon/mpri-272-exo1

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 22 Commits
Classical.v		Classical.v
Consistency.v		Consistency.v
EqualityArithmetic.v		EqualityArithmetic.v
FormalSystem.v		FormalSystem.v
Makefile		Makefile
README		README
Translation.v		Translation.v
exo1.pdf		exo1.pdf

Repository files navigation

---COMPILATION---
To compile this Coq project, run

$ make

in the project directory. Compilation checked with the version of Coq from Jan 2017.


---MODULE DEPENDENCY---
('-->' reads as 'necessary for')

FormalSystem --> Translation --> Classical --> EqualityArithmetic --> Consistency


---INTERACTIVE MODE---
Notations using Unicode symbols are used for readability.



---NOTES---
Notations were typed using the Agda Emacs input mode.