tchajed/coq-curry-howard
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
What a Coq proof actually is
11 commits 1 branch 0 tags 51 KiB
  • Rocq Prover 46.4%
  • JavaScript 24.7%
  • CSS 23.2%
  • HTML 4.2%
  • Makefile 1.5%
Find a file
Exact
Tej Chajed 2a317fc59a
 Avoid relying on Coq.Init.Ltac
2020-04-26 14:28:03 -05:00
doc/resources Add coqdocjs 2019-09-13 12:47:53 -04:00
extra Add coqdocjs 2019-09-13 12:47:53 -04:00
.gitignore Updates for Coq v8.11 compatibility 2020-04-26 14:21:10 -05:00
.travis.yml Updates for Coq v8.11 compatibility 2020-04-26 14:21:10 -05:00
_CoqProject Add a basic working version 2019-09-13 12:40:55 -04:00
CurryHoward.v Avoid relying on Coq.Init.Ltac 2020-04-26 14:28:03 -05:00
Makefile Fix whitespace issues 2019-09-13 12:51:48 -04:00
README.md Link to the source code 2019-09-13 13:13:52 -04:00

README.md

Proofs in Coq: the details

Build Status

CurryHoward.v is an explanation of what a Coq proof really is, which turns out to be the Curry-Howard correspondence. It's written in the form of Coq file that breaks down Coq definitions and proofs into their most basic forms.