agda-stdlib icon indicating copy to clipboard operation
agda-stdlib copied to clipboard
verified publisher icon agda

Adapt to reflection interface changes

Open cmcmA20 opened this issue 1 year ago • 4 comments

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

cmcmA20 avatar May 04 '24 12:05 cmcmA20

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

gallais avatar May 06 '24 08:05 gallais

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

cmcmA20 avatar May 06 '24 17:05 cmcmA20

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

gallais avatar May 06 '24 17:05 gallais

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.

MatthewDaggitt avatar May 15 '24 05:05 MatthewDaggitt

This is against milestone Agda-2.6.5 (which doesn't exist) but Agda-2.7 is out. Is this obsolete?

JacquesCarette avatar Aug 24 '24 13:08 JacquesCarette

@JacquesCarette Sorry, I forgot about this PR! Jesper and Andreas have already merged these changes in #2432.

cmcmA20 avatar Aug 24 '24 23:08 cmcmA20