[Agda] is there a show function like haskell to show result of a running function

[Sergei Meshveliani]

On Thu, 2016-01-28 at 04:38 +0000, Mandy Martino wrote:
> Hi,
> 
> open import Algebra.RingSolver
> 
> show(solve(2 x + 3 x^2))
> 
> /home/martin/agda/gosolve.agda:3,1-25
> Missing type signature for left hand side show (solve (2 x + 3
> x^2))
> when scope checking the declaration
>   show (solve (2 x + 3 x^2))


1. RingSolver of Standard library is not for solving algebraic 
   equations.
It is for forming proofs for universal algebraic equalities.
For example,
    "find a proof for that the equality 
                           (x + 1) * (x - 1) ≈ x * x - 1 
     holds for all  x  in any ring.
    "
is done by calling `solve' with appropriate arguments.


2. For Standard library developers:

the names `RingSolver' and `solve' look misleading. Because in
mathematics, in symbolic computation, in logic, and in practice the word
`solve' usually means: to find a solution in X for some equation 
F(X) = a. 

May be, it has sense to rename it to something like respectively
RingGenEquationProver and proveEq, 
with the meaning for proofEq of 
         to prove an equality E (S(x1..xn) = T(x1..xn)) 
         "in variety"
?
(a sensible terminology for this is in the area of Equational theory and
Term rewriting).

Regards,

------
Sergei