Elektrine lite

← Feed

@BoydStephenSmithJr@hachyderm.io

Post #2945921

2026-02-14 18:46 UTC

@pepper0@aus.social This is the function that "goes missing": https://gitlab.com/bss03/type-aligned/-/blob/main/src/TypeAligned.idr?ref_type=heads#L418 If you push TypeAligned.mapOnce and TypeAligned.map into a parameters block, then https://gitlab.com/bss03/type-aligned/-/blob/main/src/TypeAligned.idr?ref_type=heads#L393 can find it to perform the (indirectly, non-uniform) recursive call. I'll start working on a simpler repro once my currently builds complete and I can task-switch without losing track of what I'm doing.

Replies (0)

No replies.