R9452/demo.ipynb
master4bc15159d309630765ecd2f…

Oct 3 2019

Add go further section
4bc15159d309
·Liu Fengyun on Oct 3 2019, 20:11.
Add proof equivalence of LEM and DNE
daf81fea91b8
·Liu Fengyun on Oct 3 2019, 17:39.
Finish proof by tactics
b579420584f5
·Liu Fengyun on Oct 3 2019, 16:18.
Remove output
c06ef9bb93fe
·Liu Fengyun on Oct 3 2019, 14:59.
WIP - proof by tactics
fe4b5d0f850a
·Liu Fengyun on Oct 3 2019, 14:56.
clean outputs
d0de388131d6
·Liu Fengyun on Oct 3 2019, 13:58.
Add first-order logic example
bbbc47e0cd07
·Liu Fengyun on Oct 3 2019, 13:16.
WIP - add content about Curry-Howard correspondence
d50e27d6339d
·Liu Fengyun on Oct 3 2019, 10:43.

WIP - functional programming in Coq
46137b8e20f1
·Liu Fengyun on Oct 2 2019, 17:15.