Skip to content

Instantly share code, notes, and snippets.

@luxbock

luxbock/hmm.lean Secret

Created August 28, 2018 15:13
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 luxbock/e8a4146ab822049da4d440adc8d7f01c to your computer and use it in GitHub Desktop.
Save luxbock/e8a4146ab822049da4d440adc8d7f01c to your computer and use it in GitHub Desktop.
Download ZIP
Raw
hmm.lean
example : ¬(p ↔ ¬p) :=
assume h,
have hpinp : p → ¬p, from h.mp, -- p → p → false
have hnpip : ¬p → p, from h.mpr, -- p → false → p
_
-- p : Prop,
-- h : p ↔ ¬p,
-- hpinp : p → ¬p,
-- hnpip : ¬p → p
-- ⊢ false
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment