Unsafe. Mark a function parameter as decreasing to suppress the non-termination effect (divstd/core/types/div: X). The compiler has a very limited termination analysis, only recognizing direct recursion on inductive datatypes. When it is clear a function has a decreasing parameter but it is not recognized as such by the compiler, you can wrap the arguments in pretend-decreasingstd/core/undiv/pretend-decreasing: forall<a> (x : a) -> a to inform the termination analysis to consider that parameter decreasing on a recursive call. Use with care to not accidentally allow actual divergence (without having that reflected in the effect type).

Unsafe. This function pretends that the given action is terminating.