To not bring inconsistencies by function declarations, Juvix requires that every function passes its termination checker. However, since this is a strong requirement, often tricky to fulfill, we give the user the possibility to skip this check in two different ways:
- Using the
terminatingkeyword to annotate function type signatures as terminating. The syntax is the following.
terminating fun : A → B;
Note that annotating a function as
terminating means that all its
function clauses pass the termination checker's criterion. To skip the
termination checker for mutual recursive functions, all the functions
involved must be annotated as
- Using the CLI global flag
juvix typecheck --no-termination MyProgram.juvix
In any case, be aware that our termination checker is limited as it only accepts a subset of recursion functions. The termination checker algorithm is a slightly modification of the algorithm for checking termination in the Foetus's language.