Algebra.Solver.Sum

Definitions

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

  Normalized arithmetic expression in a commutative
  ring (represented as an (ordered) sum of terms).

Totality: total
Visibility: public export
Constructors:

Nil : Sum a as

(::) : Term a as -> Sum a as -> Sum a as

(+) : (0 _ : Rig a z o p m) -> ((v : a) -> Maybe (v = z)) -> a -> a -> a

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

(*) : (0 _ : Rig a z o p m) -> ((v : a) -> Maybe (v = z)) -> a -> a -> a

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 9

eterm : (0 _ : Rig a z o p m) -> ((v : a) -> Maybe (v = z)) -> Term a as -> a

Totality: total
Visibility: public export

esum : (0 _ : Rig a z o p m) -> ((v : a) -> Maybe (v = z)) -> Sum a as -> a

  Evaluate a sum of terms.

Totality: total
Visibility: public export

add : (0 _ : Rig a z o p m) -> ((v : a) -> Maybe (v = z)) -> Sum a as -> Sum a as -> Sum a as

  Add two sums of terms.
  
  The order of terms will be kept. If two terms have identical
  products of variables, they will be unified by adding their
  factors.

Totality: total
Visibility: public export

normSum : (0 _ : Rig a z o p m) -> ((v : a) -> Maybe (v = z)) -> Sum a as -> Sum a as

  Normalize a sum of terms by removing all terms with a
  `zero` factor.

Totality: total
Visibility: public export

mult1 : (0 _ : Rig a z o p m) -> ((v : a) -> Maybe (v = z)) -> Term a as -> Sum a as -> Sum a as

  Multiplies a single term with a sum of terms.

Totality: total
Visibility: public export

mult : (0 _ : Rig a z o p m) -> ((v : a) -> Maybe (v = z)) -> Sum a as -> Sum a as -> Sum a as

  Multiplies two sums of terms.

Totality: total
Visibility: public export

0 padd : (0 r : Rig a z o p m) -> (isZ : ((v : a) -> Maybe (v = z))) -> (x : Sum a as) -> (y : Sum a as) -> esum x + esum y = esum (add x y)

Totality: total
Visibility: export

0 pmult : (0 r : Rig a z o p m) -> (isZ : ((v : a) -> Maybe (v = z))) -> (x : Sum a as) -> (y : Sum a as) -> esum x * esum y = esum (mult x y)

Totality: total
Visibility: export

0 pnormSum : (0 r : Rig a z o p m) -> (isZ : ((v : a) -> Maybe (v = z))) -> (s : Sum a as) -> esum (normSum s) = esum s

Totality: total
Visibility: export