Unsafe primitives to dismiss divergence.


fun pretend-decreasing( x : a ) : a

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).

fun pretend-no-div( action : () -> <divstd/core/types/div: X|e> a ) : e a

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

private import std/core/typesstd/core/types