This module contains Plausible.Testable and Plausible.PrintableProb instances for mathlib types.

instance Plausible.Testable.factTestable {p : Prop} [Plausible.Testable p] : Plausible.Testable (Fact p)

Equations

• Plausible.Testable.factTestable = { run := fun (cfg : Plausible.Configuration) (min : Bool) => do let h ← Plausible.Testable.runProp p cfg min pure (Plausible.TestResult.iff ⋯ h) }

instance Plausible.Fact.printableProp {p : Prop} [Plausible.PrintableProp p] : Plausible.PrintableProp (Fact p)

Equations

• Plausible.Fact.printableProp = { printProp := Plausible.printProp p }