idris2-elab-util issues

Results 4 idris2-elab-util issues

Sort by recently updated

Elaborator really slow on types with lots of constructors

Hi, I'm trying to derive Show and Eq for a big type with approximately 200 constructors. ``` %language ElabReflection data Key : Type where KC_NO : Key KC_TRANSPARENT : Key...

locallycompact

Break-down explanation expected in Interface Implementations for Enumerations

In `Enum2.md` _Interface Implementation, Part 2_, stated "We will break this down in a moment. First, we check whether it actually works:" And we never did ...

KySpace

Update reflection code to be compatible with Idris2#2535

[Idris2#2535](github.com/idris-lang/Idris2/pull/2535) adds a quantity argument to PCase and ICase. Update the reflection code to include this additional argument. The fix in `src/Language/Reflection/Syntax.idr` is only temporary. There's some discussion in the...

ohad