WeightedNetKAT.Instances.Boolean

source

def BoolRing :

Type

Equations

BoolRing = Bool

Instances For

source

@[implicit_reducible]

instance instDecidableEqBoolRing :

DecidableEq BoolRing

Equations

instDecidableEqBoolRing = instDecidableEqBoolRing._aux_1

source

@[implicit_reducible]

instance instHOrBoolRing :

HOr BoolRing BoolRing BoolRing

Equations

instHOrBoolRing = { hOr := or }

source

@[implicit_reducible]

instance instHAndBoolRing :

HAnd BoolRing BoolRing BoolRing

Equations

instHAndBoolRing = { hAnd := and }

source

@[implicit_reducible]

instance instAddBoolRing :

Add BoolRing

Equations

instAddBoolRing = { add := or }

source

@[implicit_reducible]

instance instMulBoolRing :

Mul BoolRing

Equations

instMulBoolRing = { mul := and }

source

@[implicit_reducible]

instance instZeroBoolRing :

Zero BoolRing

Equations

instZeroBoolRing = { zero := false }

source

@[implicit_reducible]

instance instOneBoolRing :

One BoolRing

Equations

instOneBoolRing = { one := true }

source

@[simp]

theorem BoolRing.add_eq_or {a b : BoolRing} :

a + b = (a || b)

source

@[simp]

theorem BoolRing.mul_eq_and {a b : BoolRing} :

a * b = (a && b)

source

@[simp]

theorem BoolRing.zero_eq_false :

0 = false

source

@[simp]

theorem BoolRing.one_eq_true :

1 = true

source

@[implicit_reducible]

instance instSemiringBoolRing :

Semiring BoolRing

Equations

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

source

@[implicit_reducible]

instance instPartialOrderBoolRing :

PartialOrder BoolRing

Equations

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

source

@[implicit_reducible]

noncomputable instance instCompleteLatticeBoolRing :

CompleteLattice BoolRing

Equations

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

source

@[implicit_reducible]

noncomputable instance instOmegaCompletePartialOrderBoolRing :

OmegaCompletePartialOrder BoolRing

Equations

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

source

instance instMulLeftMonoBoolRing :

MulLeftMono BoolRing

source

instance instMulRightMonoBoolRing :

MulRightMono BoolRing

source

instance instIsPositiveOrderedAddMonoidBoolRing :

IsPositiveOrderedAddMonoid BoolRing

source

instance instOmegaContinuousNonUnitalSemiringBoolRing :

OmegaContinuousNonUnitalSemiring BoolRing

source

@[implicit_reducible]

instance instKStarBoolRing :

KStar BoolRing

Equations

instKStarBoolRing = { kstar := fun (x : BoolRing) => true }

source

instance instLawfulKStarBoolRing :

LawfulKStar BoolRing