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 ] Eq implementations, and TTImp change #33

Closed gallais closed 2 years ago

gallais commented 2 years ago

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

stefan-hoeck commented 2 years ago

I'll merge this right away, but please note that in an hour I'll be away for two days, so I won't be able to fix the CI until Monday next week.