search

stefan-hoeck / idris2-elab-util

Utilities and documentation for exploring idirs2's new elaborator reflection.
BSD 2-Clause "Simplified" License
76 stars 16 forks source link

[ fix ] Records now can have DataOpts #46

Closed gallais closed 2 years ago

gallais commented 2 years ago

The changes are needed by upstream for https://github.com/idris-lang/Idris2/pull/2658

buzden commented 2 years ago

I've checked this locally, all works. Since this is the only what's left for the upstream issue, I'll merge. @gallais I hope you merge upsteam one today, so that we won't have diverging nightly build in pack.

stefan-hoeck commented 2 years ago

Thanks for merging, @buzden.