instance instIsPositiveOrderedAddMonoidENat : IsPositiveOrderedAddMonoid ℕ∞

instance instOmegaContinuousNonUnitalSemiringENat : OmegaContinuousNonUnitalSemiring ℕ∞

@[implicit_reducible]

instance instKStarENat_weightedNetKAT : KStar ℕ∞

Equations

• instKStarENat_weightedNetKAT = { kstar := fun (x : ℕ∞) => match x with | some 0 => 1 | x => ⊤ }

instance instLawfulKStarENat : LawfulKStar ℕ∞