Do we have unpacked eliminators in this library?

Open JacquesCarette opened this issue 5 years ago • 2 comments

https://github.com/agda/agda/issues/4419 documents that they can be quite slow.

In some places, I think variants of Yoneda is used in this way. Anything that can speed up typechecking it worth it.

Mar 19 '20 20:03 JacquesCarette

Anything that can speed up typechecking it worth it.

Cf. agda/agda-stdlib#1105 for profiling options

Mar 19 '20 20:03 gallais

I actually ran a full load of this library with those options turned on. I have the results saved somewhere, I'll upload 'soon'.

Mar 19 '20 20:03 JacquesCarette