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

[Sergei Meshveliani]

On Thu, 2016-01-28 at 14:19 +0100, Nils Anders Danielsson wrote:
> 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.
> 

But probably  XorRingSolver  presents a different universal algebra than
RingSolver.  The prefix `Xor' probably points that there is added a
law  
      X + X = 0,

where _+_ stands for xor.

And my explanation was about  RingSolver.

Still I doubt about my explanation. 
RingSolver  may present universal algebras which are somehow near
CommutativeRing. So far, I cannot describe precisely.

Regards,

------
Sergei