@amy I do not like LLMs but I do admit that I love Agda more than I hate LLMs. Perhaps it was naive of me to believe there might be a possible compromise that is at least somewhat acceptable to everyo