The Coq mailing list

[Nils Anders Danielsson <nad AT Cs.Nott.AC.UK>]

On 2008-11-20 12:05, Edsko de Vries wrote:

> > fix-fac-ind : {g : Nat -> D Nat} {n k : Nat}
> >            -> fix-aux g fac-aux n ↓ k
> >            -> fix-aux (fac-aux g) fac-aux (suc n) ↓ suc n * k
> > fix-fac-ind {g} {n} pf with fac-aux g n ⋆
> > fix-fac-ind {g} {n} {k} converge-now | inl .k = converge-now
> > fix-fac-ind (converge-later pf) | inr y = converge-later (fix-fac-ind pf)

> I don't know Agda very well, but there is some magic going on in 
> fix-fac-ind!

The magic is called "magic with" (but is not really magic). See
http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Docs.MagicWith
for a quick explanation. Definitions using magic with can be translated
into equivalent definitions which do not use with, see Ulf Norell's
thesis for a detailed story.

--
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.