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

[ refactor] derive under elab so that additional queries and error reporting can be done #41

Closed MarcelineVQ closed 2 years ago

MarcelineVQ commented 2 years ago

While working on some tooling using elab-util I've found I need more power available at the call site for queries about what's in scope and for the ability to report errors along the way, updating derive to return a value under Elab was the most direct solution I could find to the problem.

MarcelineVQ commented 2 years ago

re https://github.com/MarcelineVQ/blessed-derive

MarcelineVQ commented 2 years ago

Decided to keep these changes relegated to my own lib for now, as the lib has been rapidly changing