[Agda] Quoting mutual definition

[Ulf Norell]

The information isn't available directly, but you could do the dependency
analysis yourself by traversing the constructor types and looking up the
definition of encountered names to see which refer back to the type in
question.

/ Ulf

On Mon, Apr 29, 2019 at 1:13 PM Liang-Ting Chen <
liang.ting.chen.tw at gmail.com> wrote:

> Hi all,
>
> I am writing a tactic generating the elimination rule for dependent type,
> i.e. the `destruct` tactic in Coq, using Agda's reflection mechanism.
> However, it seems impossible to know if a definition is mutually defined or
> not as this information is not exposed unless it is given manually. Is that
> right?
>
> For example, suppose two data types are mutually defined
>
> mutual
>   data Even : ℕ → Set where
>     z  : Even 0
>     2n : Odd n → Even (suc n)
>   data Odd : ℕ → Set where
>     s  : Even n → Odd (suc n)
>
> By quoting `Even` or any term of `Even`, I want to know that `Odd` is also
> part of the mutual definition so that the following elimination rule can be
> generated
>
> module _ {P : ∀ n → Even n → Set} {Q : ∀ n → Odd n → Set}
>   (Pz : P 0 z)(Pss : ∀ n o → Q n o → P (suc n) (ss o)) (Pone : ∀ n e → P n
> e → Q (suc n) (one e)) where
>   mutual
>     elimEven : ∀ n → (e : Even n) → P n e
>     elimEven .0 z = Pz
>     elimEven .(suc _) (ss x) = Pss _ x  (elimOdd _ x)
>
>     elimOdd  : ∀ n → (o : Odd n) → Q n o
>     elimOdd .(suc _) (one x) = Pone _ x (elimEven _ x)
>
> Or, if there is any workaround, please let me know! Thanks.
> --
> Best regards,
> Liang-Ting
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190429/8d920915/attachment.html>