twitchcoq

Reimplementing a subset of Coq in Python

Just kidding, Coq is too complex. We implemented metamath instead.

random notes

First order logic:

Theorem test : exists x : nat, x + 2 = 4.
Theorem test2 : forall y : nat, (exists x : nat, x = y).

Second order logic (quantifing over first order logic statements):

forall y : (fun x : nat -> nat)

Higher order logic...so on and so forth