[Agda] Re: _iff_
Serge D. Mechveliani
mechvel at botik.ru
Tue Apr 2 16:56:59 CEST 2013
To my request of
>> And introduce
>> A iff' B = (A -> B) \times (B -> A)
>> for this.
>> But can this be written in a nicer way by using Standard library?
Nils Anders Danielsson wrote on Apr 2 2013
> You may want to use Function.Equivalence._<=>_.
(I copy `_<=>_' from the letter on the web page).
> However, this type is defined as a special case of a more general
> definition that uses setoids, and can be somewhat awkward to use.
Well, it works. It is what I asked for.
I have seen \r= and \l=, and the problem was to guess to grep for
the \iff math symbol in the source.
More information about the Agda