search

stefan-hoeck / idris2-elab-util

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

[ fix ] Necessary changes for PR #2816 #58

Closed gallais closed 1 year ago

gallais commented 1 year ago

Note that I haven't checked that the output of the REPL commands in the Doc modules is still valid after this update.

buzden commented 1 year ago

I've checked everything with pack build elab-util && pack build elab-util-docs && pack test elab-util with compiler version at the upstream PR and all worked. @gallais I can merge it now as soon as the upstream PR would be merged today (as usual, to not to create a bad night build).

gallais commented 1 year ago

Happy to merge today

buzden commented 1 year ago

By the way, output of REPL in docs doesn't change because of implementation of Pretty (Maybe a) which uses pretty of Pretty a in the Just case O_O

stefan-hoeck commented 1 year ago

Thanks for this. I'm in the process of using new pretty printers and ditching the dependency on contrib, so I'll have to recheck the REPL output anyway.