Idris2Doc : Algebra.Solver.Semiring.Util

Algebra.Solver.Semiring.Util

(source)
Reexports
import public Syntax.PreorderReasoning
Definitions
0 p213 : {auto {conArg:808} : Semiring a} -> k + (m + n) = m + (k + n)
  Totality: total
  Visibility: export
0 p1324 : {auto {conArg:954} : Semiring a} -> (k + l) + (m + n) = (k + m) + (l + n)
  Totality: total
  Visibility: export
0 m1324 : {auto {conArg:1214} : Semiring a} -> (k * l) * (m * n) = (k * m) * (l * n)
  Totality: total
  Visibility: export