@tristanC They aren't migrating if I understood correctly. Just need a way to produce TS apps from Agda sources and LLM translation happens to do a better job at it than a "real" compiler.
QOTO: Question Others to Teach Ourselves An inclusive, Academic Freedom, instance All cultures welcome. Hate speech and harassment strictly forbidden.
