Hoogle Search

Within LTS Haskell 24.26 (ghc-9.10.3)

Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.

  1. supportsPseudoBooleans :: SolverCapabilities -> Bool

    sbv Data.SBV.Internals

    Supports pseudo-boolean operations?

  2. KBool :: Kind

    sbv Data.SBV.Trans

    No documentation available.

  3. type SBool = SBV Bool

    sbv Data.SBV.Trans

    A symbolic boolean/bit

  4. fromBool :: Bool -> SBool

    sbv Data.SBV.Trans

    Conversion from Bool to SBool

  5. isBoolean :: HasKind a => a -> Bool

    sbv Data.SBV.Trans

    No documentation available.

  6. sBool :: MonadSymbolic m => String -> m SBool

    sbv Data.SBV.Trans

    Generalization of sBool

  7. sBools :: MonadSymbolic m => [String] -> m [SBool]

    sbv Data.SBV.Trans

    Generalization of sBools

  8. shefferBooleanAlgebra :: IO BooleanAlgebraProof

    sbv Documentation.SBV.Examples.KnuckleDragger.ShefferStroke

    Prove that Sheffer stroke axioms imply it is a boolean algebra. We have: 

    >>> shefferBooleanAlgebra
Axiom: ﬧﬧa == a
Axiom: a ⏐ (b ⏐ ﬧb) == ﬧa
Axiom: ﬧ(a ⏐ (b ⏐ c)) == (ﬧb ⏐ a) ⏐ (ﬧc ⏐ a)
Lemma: a | b = b | a
Step: 1 (ﬧﬧa == a)                                        Q.E.D.
Step: 2 (ﬧﬧa == a)                                        Q.E.D.
Step: 3                                                   Q.E.D.
Step: 4 (ﬧ(a ⏐ (b ⏐ c)) == (ﬧb ⏐ a) ⏐ (ﬧc ⏐ a))           Q.E.D.
Step: 5                                                   Q.E.D.
Step: 6 (ﬧﬧa == a)                                        Q.E.D.
Step: 7 (ﬧﬧa == a)                                        Q.E.D.
Result:                                                   Q.E.D.
Lemma: a | a′ = b | b′
Step: 1 (ﬧﬧa == a)                                        Q.E.D.
Step: 2 (a ⏐ (b ⏐ ﬧb) == ﬧa)                              Q.E.D.
Step: 3                                                   Q.E.D.
Step: 4 (a ⏐ (b ⏐ ﬧb) == ﬧa)                              Q.E.D.
Step: 5 (ﬧﬧa == a)                                        Q.E.D.
Result:                                                   Q.E.D.
Lemma: a ⊔ b = b ⊔ a                                        Q.E.D.
Lemma: a ⊓ b = b ⊓ a                                        Q.E.D.
Lemma: a ⊔ ⲳ = a                                            Q.E.D.
Lemma: a ⊓ т = a                                            Q.E.D.
Lemma: a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c)                      Q.E.D.
Lemma: a ⊓ (b ⊔ c) = (a ⊓ b) ⊔ (a ⊓ c)                      Q.E.D.
Lemma: a ⊔ aᶜ = т                                           Q.E.D.
Lemma: a ⊓ aᶜ = ⲳ                                           Q.E.D.
Lemma: a ⊔ т = т
Step: 1                                                   Q.E.D.
Step: 2                                                   Q.E.D.
Step: 3                                                   Q.E.D.
Step: 4                                                   Q.E.D.
Step: 5                                                   Q.E.D.
Step: 6                                                   Q.E.D.
Result:                                                   Q.E.D.
Lemma: a ⊓ ⲳ = ⲳ
Step: 1                                                   Q.E.D.
Step: 2                                                   Q.E.D.
Step: 3                                                   Q.E.D.
Step: 4                                                   Q.E.D.
Step: 5                                                   Q.E.D.
Step: 6                                                   Q.E.D.
Result:                                                   Q.E.D.
Lemma: a ⊔ (a ⊓ b) = a
Step: 1                                                   Q.E.D.
Step: 2                                                   Q.E.D.
Step: 3                                                   Q.E.D.
Step: 4                                                   Q.E.D.
Step: 5                                                   Q.E.D.
Result:                                                   Q.E.D.
Lemma: a ⊓ (a ⊔ b) = a
Step: 1                                                   Q.E.D.
Step: 2                                                   Q.E.D.
Step: 3                                                   Q.E.D.
Step: 4                                                   Q.E.D.
Step: 5                                                   Q.E.D.
Result:                                                   Q.E.D.
Lemma: a ⊓ a = a
Step: 1                                                   Q.E.D.
Step: 2                                                   Q.E.D.
Result:                                                   Q.E.D.
Lemma: a ⊔ a' = т → a ⊓ a' = ⲳ → a' = aᶜ
Step: 1                                                   Q.E.D.
Step: 2                                                   Q.E.D.
Step: 3                                                   Q.E.D.
Step: 4                                                   Q.E.D.
Step: 5                                                   Q.E.D.
Step: 6                                                   Q.E.D.
Step: 7                                                   Q.E.D.
Step: 8                                                   Q.E.D.
Step: 9                                                   Q.E.D.
Step: 10                                                  Q.E.D.
Step: 11                                                  Q.E.D.
Result:                                                   Q.E.D.
Lemma: aᶜᶜ = a                                              Q.E.D.
Lemma: aᶜ = bᶜ → a = b                                      Q.E.D.
Lemma: a ⊔ bᶜ = т → a ⊓ bᶜ = ⲳ → a = b                      Q.E.D.
Lemma: a ⊔ (aᶜ ⊔ b) = т
Step: 1                                                   Q.E.D.
Step: 2                                                   Q.E.D.
Step: 3                                                   Q.E.D.
Step: 4                                                   Q.E.D.
Step: 5                                                   Q.E.D.
Step: 6                                                   Q.E.D.
Result:                                                   Q.E.D.
Lemma: a ⊓ (aᶜ ⊓ b) = ⲳ
Step: 1                                                   Q.E.D.
Step: 2                                                   Q.E.D.
Step: 3                                                   Q.E.D.
Step: 4                                                   Q.E.D.
Step: 5                                                   Q.E.D.
Step: 6                                                   Q.E.D.
Result:                                                   Q.E.D.
Lemma: (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ                                   Q.E.D.
Lemma: (a ⨅ b)ᶜ = aᶜ ⨆ bᶜ                                   Q.E.D.
Lemma: (a ⊔ (b ⊔ c)) ⊔ aᶜ = т                               Q.E.D.
Lemma: b ⊓ (a ⊔ (b ⊔ c)) = b                                Q.E.D.
Lemma: b ⊔ (a ⊓ (b ⊓ c)) = b                                Q.E.D.
Lemma: (a ⊔ (b ⊔ c)) ⊔ bᶜ = т
Step: 1                                                   Q.E.D.
Step: 2                                                   Q.E.D.
Step: 3                                                   Q.E.D.
Step: 4                                                   Q.E.D.
Step: 5                                                   Q.E.D.
Step: 6                                                   Q.E.D.
Step: 7                                                   Q.E.D.
Step: 8                                                   Q.E.D.
Step: 9                                                   Q.E.D.
Result:                                                   Q.E.D.
Lemma: (a ⊔ (b ⊔ c)) ⊔ cᶜ = т                               Q.E.D.
Lemma: (a ⊔ b ⊔ c)ᶜ ⊓ a = ⲳ
Step: 1                                                   Q.E.D.
Step: 2                                                   Q.E.D.
Step: 3                                                   Q.E.D.
Step: 4                                                   Q.E.D.
Step: 5                                                   Q.E.D.
Step: 6                                                   Q.E.D.
Step: 7                                                   Q.E.D.
Step: 8                                                   Q.E.D.
Step: 9                                                   Q.E.D.
Result:                                                   Q.E.D.
Lemma: (a ⊔ b ⊔ c)ᶜ ⊓ b = ⲳ                                 Q.E.D.
Lemma: (a ⊔ b ⊔ c)ᶜ ⊓ c = ⲳ                                 Q.E.D.
Lemma: (a ⊔ (b ⊔ c)) ⊔ ((a ⊔ b) ⊔ c)ᶜ = т
Step: 1                                                   Q.E.D.
Step: 2                                                   Q.E.D.
Step: 3                                                   Q.E.D.
Step: 4                                                   Q.E.D.
Step: 5                                                   Q.E.D.
Step: 6                                                   Q.E.D.
Step: 7                                                   Q.E.D.
Step: 8                                                   Q.E.D.
Result:                                                   Q.E.D.
Lemma: (a ⊔ (b ⊔ c)) ⊓ ((a ⊔ b) ⊔ c)ᶜ = ⲳ
Step: 1                                                   Q.E.D.
Step: 2                                                   Q.E.D.
Step: 3                                                   Q.E.D.
Step: 4                                                   Q.E.D.
Step: 5                                                   Q.E.D.
Step: 6                                                   Q.E.D.
Step: 7                                                   Q.E.D.
Step: 8                                                   Q.E.D.
Step: 9                                                   Q.E.D.
Step: 10                                                  Q.E.D.
Step: 11                                                  Q.E.D.
Step: 12                                                  Q.E.D.
Result:                                                   Q.E.D.
Lemma: a ⊔ (b ⊔ c) = (a ⊔ b) ⊔ c                            Q.E.D.
Lemma: a ⊓ (b ⊓ c) = (a ⊓ b) ⊓ c
Step: 1                                                   Q.E.D.
Step: 2                                                   Q.E.D.
Step: 3                                                   Q.E.D.
Result:                                                   Q.E.D.
Lemma: a ≤ b → b ≤ a → a = b
Step: 1                                                   Q.E.D.
Step: 2                                                   Q.E.D.
Step: 3                                                   Q.E.D.
Result:                                                   Q.E.D.
Lemma: a ≤ a                                                Q.E.D.
Lemma: a ≤ b → b ≤ c → a ≤ c
Step: 1                                                   Q.E.D.
Step: 2                                                   Q.E.D.
Step: 3                                                   Q.E.D.
Step: 4                                                   Q.E.D.
Result:                                                   Q.E.D.
Lemma: a < b ↔ a ≤ b ∧ ¬b ≤ a                               Q.E.D.
Lemma: a ≤ a ⊔ b                                            Q.E.D.
Lemma: b ≤ a ⊔ b                                            Q.E.D.
Lemma: a ≤ c → b ≤ c → a ⊔ b ≤ c
Step: 1                                                   Q.E.D.
Step: 2                                                   Q.E.D.
Result:                                                   Q.E.D.
Lemma: a ⊓ b ≤ a                                            Q.E.D.
Lemma: a ⊓ b ≤ b                                            Q.E.D.
Lemma: a ≤ b → a ≤ c → a ≤ b ⊓ c
Step: 1                                                   Q.E.D.
Step: 2                                                   Q.E.D.
Step: 3                                                   Q.E.D.
Result:                                                   Q.E.D.
Lemma: (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z                        Q.E.D.
Lemma: x ⊓ xᶜ ≤ ⊥                                           Q.E.D.
Lemma: ⊤ ≤ x ⊔ xᶜ                                           Q.E.D.
Lemma: a ≤ ⊤
Step: 1                                                   Q.E.D.
Step: 2                                                   Q.E.D.
Step: 3                                                   Q.E.D.
Result:                                                   Q.E.D.
Lemma: ⊥ ≤ a
Step: 1                                                   Q.E.D.
Step: 2                                                   Q.E.D.
Result:                                                   Q.E.D.
Lemma: x \ y = x ⊓ yᶜ                                       Q.E.D.
Lemma: x ⇨ y = y ⊔ xᶜ                                       Q.E.D.
BooleanAlgebraProof {
le_refl         : [Proven] a ≤ a
le_trans        : [Proven] a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le: [Proven] a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm     : [Proven] a ≤ b → b ≤ a → a = b
le_sup_left     : [Proven] a ≤ a ⊔ b
le_sup_right    : [Proven] b ≤ a ⊔ b
sup_le          : [Proven] a ≤ c → b ≤ c → a ⊔ b ≤ c
inf_le_left     : [Proven] a ⊓ b ≤ a
inf_le_right    : [Proven] a ⊓ b ≤ b
le_inf          : [Proven] a ≤ b → a ≤ c → a ≤ b ⊓ c
le_sup_inf      : [Proven] (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
inf_compl_le_bot: [Proven] x ⊓ xᶜ ≤ ⊥
top_le_sup_compl: [Proven] ⊤ ≤ x ⊔ xᶜ
le_top          : [Proven] a ≤ ⊤
bot_le          : [Proven] ⊥ ≤ a
sdiff_eq        : [Proven] x \ y = x ⊓ yᶜ
himp_eq         : [Proven] x ⇨ y = y ⊔ xᶜ
}

  9. pBoolean :: Parser AST

    simple-templates Web.Simple.Templates.Parser

    No documentation available.

  10. data SBool (b :: Bool)

    singleraeh Singleraeh.Bool

    Singleton Bool.

Page 137 of many | Previous | Next