Idris2Doc : Algebra.Solver.CommutativeMonoid

Algebra.Solver.CommutativeMonoid

(source)
Reexports
import public Algebra.Monoid
import public Algebra.Solver.Prod
Definitions
times : CommutativeMonoid a => Nat -> a -> a
  Totality: total
  Visibility: public export
data Expr : (a : Type) -> List a -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Lit : a -> Expr a as
  
Var : (x : a) -> Elem x as -> Expr a as
  
Neutral : Expr a as
  
Append : Expr a as -> Expr a as -> Expr a as

  Hints:
  
FromString a => FromString (Expr a as)
  
Monoid (Expr a as)
  
Semigroup (Expr a as)
record Term : (a : Type) -> List a -> Type
  Totality: total
  Visibility: public export
  Constructor: 
T : a -> Prod a as -> Term a as

  Projections:
  
.factor : Term a as -> a
  
.prod : Term a as -> Prod a as
.factor : Term a as -> a
  Totality: total
  Visibility: public export
factor : Term a as -> a
  Totality: total
  Visibility: public export
.prod : Term a as -> Prod a as
  Totality: total
  Visibility: public export
prod : Term a as -> Prod a as
  Totality: total
  Visibility: public export
append : CommutativeMonoid a => Term a as -> Term a as -> Term a as
  Totality: total
  Visibility: public export
normalize : CommutativeMonoid a => Expr a as -> Term a as
  Totality: total
  Visibility: public export
eval : CommutativeMonoid a => Expr a as -> a
  Totality: total
  Visibility: public export
eprod : CommutativeMonoid a => Prod a as -> a
  Totality: total
  Visibility: public export
eterm : CommutativeMonoid a => Term a as -> a
  Totality: total
  Visibility: public export
0 pvar : {auto {conArg:1889} : CommutativeMonoid a} -> (as : List a) -> (e : Elem x as) -> eprod (fromVar e) = x
  Totality: total
  Visibility: export
0 solve : {auto {conArg:3210} : CommutativeMonoid a} -> (as : List a) -> (e1 : Expr a as) -> (e2 : Expr a as) -> normalize e1 = normalize e2 => eval e1 = eval e2
  Totality: total
  Visibility: export