Skip to content

Instantly share code, notes, and snippets.

@stevenfontanella

stevenfontanella/Existential.txt Secret

Created December 27, 2021 21:56
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save stevenfontanella/c26bfbf79f615ae0145ae4704df8b47f to your computer and use it in GitHub Desktop.
Save stevenfontanella/c26bfbf79f615ae0145ae4704df8b47f to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Existential.txt
exists a. a
\/ a -- (disjunction forall types t in T e.g. t1 \/ t2 \/ t3 ...)
¬¬ \/ a -- double negation
¬ (/\ ¬a) -- de morgan
-- side proof ¬a == a -> Void --
¬a
False \/ ¬a -- Identity
a -> False -- Definition of ->
-- done --
¬ (/\ ¬a)
¬ (/\ a -> Void)
(/\ a -> Void) -> Void
(forall a. a -> Void) -> Void
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment