[Agda] Quoting mutual definition

[Apostolis Xekoukoulotakis]

If the information is kept, that would be useful for backends as well.

On Mon, Apr 29, 2019 at 6:13 PM Liang-Ting Chen <
liang.ting.chen.tw at gmail.com> wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190429/d1a8c9ea/attachment.html>