Algebra.Solver.Prod

Reexports

Definitions

data Prod : (a : Type) -> List a -> Type

  A product of variables each represented by the exponent,
  to which it is raised.
  
  When normalizing arithmetic expressions, they often
  get converted to (sums of) products of variables
  (listed in index `as`), each raised to a certain
  exponent. This is the case for commutative monoids
  (a single product) as well as commutative (semi)rings
  (a sum of products).

Totality: total
Visibility: public export
Constructors:

Nil : Prod a []

(::) : Nat -> Prod a xs -> Prod a (x :: xs)

mult : Prod a as -> Prod a as -> Prod a as

  Multiplying two products means adding all
  expontents pairwise.

Totality: total
Visibility: public export

compProd : Prod a as -> Prod a as -> Ordering

  We sort products by lexicographically comparing
  the exponents.

Totality: total
Visibility: public export

one : Prod a as

  The neutral product where all exponents are zero.

Totality: total
Visibility: public export

fromVar : Elem x as -> Prod a as

  Convert a single variable to a product of variables.

Totality: total
Visibility: public export

0 pcompNat : (x : Nat) -> (y : Nat) -> compare x y = EQ -> x = y

Totality: total
Visibility: export

0 pcompProd : (x : Prod a as) -> (y : Prod a as) -> compProd x y = EQ -> x = y

Totality: total
Visibility: export