[Agda] expressing iff
Serge D. Mechveliani
mechvel at botik.ru
Tue Apr 2 10:23:05 CEST 2013
as lib-0.7 has \r= for inclusion, may be it also has something
ready for `iff' ? -- the one that also coveres the below example.
It looks a bit strange for a user to introduce such `iff'.
May be, Standard library needs to add such?
On Tue, Apr 02, 2013 at 09:10:15AM +0200, Andreas Abel wrote:
> Looks fine to me. --Andreas
> On 01.04.13 1:09 AM, Serge D. Mechveliani wrote:
> >Dear all,
> >I need to express a relation like
> > p x y (: Bool) if and only iff f x \~~ f y holds
> > (is not empty).
> >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?
> >The code with math symbols is attached here as t.agda.zip.
More information about the Agda