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

[ upstream ] ICase takes an extra argument #72

Closed gallais closed 1 year ago

gallais commented 1 year ago

Cf. https://github.com/idris-lang/Idris2/pull/3062

buzden commented 1 year ago

Since this is a technical change, I can merge it now, once upstream PR is ready

gallais commented 1 year ago

I think the PR is ready.

buzden commented 1 year ago

@gallais sync ;-)