class ValueType (T : Type) extends Zero T, AddCommSemigroup T, Sub T, Mul T, LinearOrder T : Type

• zero : T
• add : T → T → T
• add_assoc (a b c : T) : a + b + c = a + (b + c)
• add_comm (a b : T) : a + b = b + a
• sub : T → T → T
• mul : T → T → T
• le : T → T → Prop
• lt : T → T → Prop
• le_refl (a : T) : a ≤ a
• le_trans (a b c : T) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : T) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : T) : a ≤ b → b ≤ a → a = b
• min : T → T → T
• max : T → T → T
• compare : T → T → Ordering
• le_total (a b : T) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE T
• toDecidableEq : DecidableEq T
• toDecidableLT : DecidableLT T
• min_def (a b : T) : min a b = if a ≤ b then a else b
• max_def (a b : T) : max a b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : T) : compare a b = compareOfLessAndEq a b

instance instValueTypeSumOfHasAltLinearOrderOfSemiringWithMonus {V K : Type} [ValueType V] [HasAltLinearOrder K] [SemiringWithMonus K] : ValueType (V ⊕ K)

Equations

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

instance instToStringSum_provenance {V : Type u_1} {K : Type u_2} [ToString V] [ToString K] : ToString (V ⊕ K)

Equations

• instToStringSum_provenance = { toString := fun (a : V ⊕ K) => match a with | Sum.inl a => toString a | Sum.inr a => toString a }