关于不终止的问题With clauses obscuring termination答案建议求助于 <-wellFounded .
我查看了 <-wellFounded 的定义之前，让我印象深刻的是有一个 --safe在OPTIONS 。如果没有这个选项，它是否也可以工作？也就是说，正在使用 --safe进行一些优化，还是解决一些基本问题？那么在这种情况下，我们只是将终止问题委托(delegate)给标记为“安全”的函数？
最佳答案
这是完全安全的。 --safe 让模块遵守比默认更严格的标准。这并不意味着某些东西不安全，而是意味着某些东西是安全的。从任何模块使用有根据的递归，无论安全与否，都不会引入非终止。终止相当强烈地融入到可访问性的归纳定义中。
关于agda - Well-Founded 递归安全吗？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/58846127/