<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr">Hi all, <div><br></div><div>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? </div><div><div><br></div><div>For example, suppose two data types are mutually defined </div><div><br></div><div><div>mutual</div><div>  data Even : ℕ → Set where</div><div>    z  : Even 0</div><div>    2n : Odd n → Even (suc n)</div><div>  data Odd : ℕ → Set where</div><div>    s  : Even n → Odd (suc n)</div></div><div><br></div><div>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</div><div><br></div><div><div>module _ {P : ∀ n → Even n → Set} {Q : ∀ n → Odd n → Set}</div><div>  (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</div><div>  mutual</div><div>    elimEven : ∀ n → (e : Even n) → P n e</div><div>    elimEven .0 z = Pz</div><div>    elimEven .(suc _) (ss x) = Pss _ x  (elimOdd _ x)</div><div><br></div><div>    elimOdd  : ∀ n → (o : Odd n) → Q n o</div><div>    elimOdd .(suc _) (one x) = Pone _ x (elimEven _ x)</div></div><div><br></div><div>Or, if there is any workaround, please let me know! Thanks. </div>-- <br><div dir="ltr" class="gmail-m_-5531616237424558251gmail-m_4369087461636089659gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div>Best regards,<br></div>Liang-Ting</div></div></div></div></div></div></div></div></div></div></div>