<div dir="ltr">Thanks for the useful tip! Indeed, dependency analysis would do the trick. But, as the information was given but disregarded later, would it be simpler and easier to keep this information and expose it? No idea how much effort needed to have this information available via reflection, though. -- Liang-Ting</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, 29 Apr 2019 at 12:23, Ulf Norell <<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex"><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" target="_blank">liang.ting.chen.tw@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color: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_3726191086856120590gmail-m_-6574193675997457022gmail-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>
</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="gmail-m_3726191086856120590gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div>Best regards,<br></div>Liang-Ting</div></div></div></div></div>