[Agda] Quoting mutual definition

[Liang-Ting Chen]

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

On Mon, 29 Apr 2019 at 12:23, Ulf Norell <ulf.norell at gmail.com> wrote:

> 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
>>
>

-- 
Best regards,
Liang-Ting
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190429/9c420ccb/attachment.html>