Open andreasabel opened 2 weeks ago
I think I got this one wrong. The combination of those flags just turns off termination checking completely, which Agda allows unless --safe
.
No, you got it right. There is a difference between two behaviors:
--no-termination-check
which disables termination checking as a concept. This option renders all recursive functions accepted, as they do not need to be checked for termination at all;--no-syntax-based-termination
--no-type-based-termination
, which disables all known termination checkers in the presence of termination checking as a concept. This combination of options should make all recursive functions rejected, as there is no termination checker that can certify their termination.
--no-syntax-based-termination
turns on--type-based-termination
, but should not:ATTN: @knisht