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

[Nils Anders Danielsson]

On 2016-01-28 12:56, Sergei Meshveliani wrote:
> 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.

This is not quite true. Here is an example taken from "Proving
Equalities in a Commutative Ring Done Right in Coq" by Grégoire and
Mahboubi (http://doi.org/10.1007/11541868_7):

   example : (b : Bool) → b xor b ≡ false
   example = solve 1 (λ b → b :+ b := con false) refl
     where open XorRingSolver

We don't have x + x ≡ 0 for arbitrary x in an arbitrary ring.

-- 
/NAD