[Agda] mutual recursion

[Nils Anders Danielsson]

On 2010-11-15 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?

In some (many?) cases you can get away with using a Σ, right?

   combined : (A : Tp) → Σ[ B ∶ Set ] (Tm A → B)

-- 
/NAD