def BoolFunc (X : Type) : Type

Equations

• BoolFunc X = ((X → Bool) → Bool)

instance instZeroBoolFunc {X : Type} : Zero (BoolFunc X)

Equations

• instZeroBoolFunc = { zero := fun (x : X → Bool) => decide False }

instance instAddBoolFunc {X : Type} : Add (BoolFunc X)

Equations

• instAddBoolFunc = { add := fun (f₁ f₂ : BoolFunc X) (ν : X → Bool) => f₁ ν || f₂ ν }

instance instOneBoolFunc {X : Type} : One (BoolFunc X)

Equations

• instOneBoolFunc = { one := fun (x : X → Bool) => decide True }

instance instMulBoolFunc {X : Type} : Mul (BoolFunc X)

Equations

• instMulBoolFunc = { mul := fun (f₁ f₂ : BoolFunc X) (ν : X → Bool) => f₁ ν && f₂ ν }

instance instLEBoolFunc {X : Type} : LE (BoolFunc X)

Equations

• instLEBoolFunc = { le := fun (f₁ f₂ : BoolFunc X) => ∀ (ν : X → Bool), f₁ ν ≤ f₂ ν }

instance instSubBoolFunc {X : Type} : Sub (BoolFunc X)

Equations

• instSubBoolFunc = { sub := fun (f₁ f₂ : BoolFunc X) (ν : X → Bool) => f₁ ν && !f₂ ν }

instance instCommSemiringBoolFunc {X : Type} : CommSemiring (BoolFunc X)

Equations

• One or more equations did not get rendered due to their size.

instance instSemiringWithMonusBoolFunc {X : Type} : SemiringWithMonus (BoolFunc X)

Equations

• One or more equations did not get rendered due to their size.

theorem BoolFunc.absorptive {X : Type} : _root_.absorptive (BoolFunc X)

theorem BoolFunc.idempotent {X : Type} : _root_.idempotent (BoolFunc X)

theorem BoolFunc.mul_sub_left_distributive {X : Type} : _root_.mul_sub_left_distributive (BoolFunc X)