search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
561 stars 234 forks source link

Adapt to reflection interface changes #2380

Open cmcmA20 opened 1 month ago

cmcmA20 commented 1 month ago

Downstream fix, see ~agda/agda#7247~ agda/agda#7322 Do not merge before the parent PR

gallais commented 1 month ago

I'm not a fan of just having a Bool there. Can we throw in a more informative sum type?

cmcmA20 commented 1 month ago

Yeah, feel free to suggest what other info should be exposed.

gallais commented 1 month ago

I don't mean necessarily more information but a type with informative constructor names.

MatthewDaggitt commented 1 month ago

Hi @cmcmA20, thanks for the fix! Any chance you could make this against the experimental branch rather than the master branch? Changes to Agda itself don't usually go on master.