Algebra.Solver.Monoid

Definitions

data Expr : Type -> Type

Totality: total
Visibility: public export
Constructors:

Var : a -> Expr a

Neutral : Expr a

Append : Expr a -> Expr a -> Expr a

Hints:

Monoid (Expr a)

Semigroup (Expr a)

eval : LMonoid a => Expr a -> a

Totality: total
Visibility: public export

esum : LMonoid a => List a -> a

Totality: total
Visibility: public export

normalize : Expr a -> List a

Totality: total
Visibility: public export

0 solve : {auto {conArg:1273} : LMonoid a} -> (e1 : Expr a) -> (e2 : Expr a) -> normalize e1 = normalize e2 => eval e1 = eval e2

Totality: total
Visibility: export