Algebra.Solver.Semigroup

Definitions

data Expr : Type -> Type

Totality: total
Visibility: public export
Constructors:

Var : a -> Expr a

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

Hint: 

Semigroup (Expr a)

eval : LSemigroup a => Expr a -> a

Totality: total
Visibility: public export

esum' : LSemigroup a => a -> List a -> a

Totality: total
Visibility: public export

esum : LSemigroup a => List1 a -> a

Totality: total
Visibility: public export

normalize : Expr a -> List1 a

Totality: total
Visibility: public export

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

Totality: total
Visibility: export