Skip to content

Instantly share code, notes, and snippets.

@Kazark

Kazark/NotNotLEM.idr

Last active November 13, 2018 15:17
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save Kazark/3b237e27ce1eb733b923da2c6ebf46f0 to your computer and use it in GitHub Desktop.
Save Kazark/3b237e27ce1eb733b923da2c6ebf46f0 to your computer and use it in GitHub Desktop.
Download ZIP
Intuitionist logic is by no means denying the law of excluded middle!
Raw
NotNotLEM.idr
module NotNotLEM
%default total
%access public export
notDistributesOverEither : Not (Either a b) -> (Not a, Not b)
notDistributesOverEither neither = (notLeft neither, notRight neither) where
notLeft : Not (Either a b) -> Not a
notLeft neither x = neither (Left x)
notRight : Not (Either a b) -> Not b
notRight nor y = nor (Right y)
notNotExcludedMiddle : Not (Not (Either a (Not a)))
notNotExcludedMiddle middle =
let (notA, notNotA) = notDistributesOverEither middle
in notNotA notA
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment