[Agda] mutual recursion

[Thorsten Altenkirch]

Check out Frederik Forsberg and Anton Setzer's recent CSL paper.

http://cs.swan.ac.uk/~csfnf/papers/indind_csl2010.pdf

Incidently, Frederik, Peter Morris and I were discussing a categorical semantics for those last week. Still to be written up.

Cheers,
Thorsten

On 15 Nov 2010, at 21:27, Dan Licata wrote:

> Agda allows the definition of mutually recursive functions, where one
> appears in the type of the other.  E.g. if
> 
>  Tp : Set
>  Tm : Tp -> Set
> 
> then we can define
> 
>  mutual
>    tpsem : Tp -> Set
>    tpsem = {!!} 
> 
>    tmsem : {A : Tp} -> Tm A -> tpsem A
>    tmsem = {!!}
> 
> Is there a good description somewhere of how these definitions be
> reduced to ones that don't use this feature?
> 
> -Dan
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda