[Agda] Quoting mutual definition

[Liang-Ting Chen]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190429/593edae3/attachment.html>