Skip to content

Instantly share code, notes, and snippets.

@comex

comex/foo.rs

Created April 5, 2018 05:01
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 comex/0da167c272a63f90f8a0400949487b24 to your computer and use it in GitHub Desktop.
Save comex/0da167c272a63f90f8a0400949487b24 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
foo.rs
// Prove that
// ∀p. ∀q. (p ∨ q)
// implies
// ∀p. ∀q. ¬(¬p ∧ ¬q)
pub fn foo(fa1: ForAll<ForAll<Or<DB2, DB3>>>) -> ForAll<ForAll<Not<And<Not<DB4>, Not<DB5>>>>> {
map!(fa1, |fa2: ForAll<_>| {
map!(fa2, |or: Or<_, _>| {
or.de_morgan()
})
})
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment