<div dir="ltr"><div>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.</div><div><br></div><div>/ Ulf<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Apr 29, 2019 at 1:13 PM Liang-Ting Chen <<a href="mailto:liang.ting.chen.tw@gmail.com">liang.ting.chen.tw@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><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_-7582238318305427971gmail-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>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>