Post #2775971
2026-05-12 19:52 UTC
@totbwf@types.pl @ncf@types.pl By the way, how technically feasible would it be to make Mikan translate pattern matching and recursion to eliminators?
Replies (1)
-
@ncf@types.pl 2026-05-12 20:05
@jeanas@mathstodon.xyz @totbwf@types.pl probably completely intractable unless we get rid of like half of Agda's induction features, i'm guessing