Questions tagged [termination]
The termination tag has no usage guidance.
Universe inconsistency as an effect
The Internet tells me there is some work on languages that permit general recursion but carry information about possible divergence in the type system. For instance, the simply-typed language Koka ...
Termination and confluence -- which goes first?
I'm implementing a version of cubical type theory where the well-definedness of pattern matching functions is implied by: the well-typedness of the clauses (type check) the coverage of the patterns (...
Well founded recursion through lists
I'm trying out Lean for programming, and I'm struggling with the termination checker. Here's the toy I'm playing with: ...
How to convince Agda that definition is terminating in the presence of unapplied recursion?
In the following, termination check fails for Df: ...
Strictly-monotone "max" operation for constructive Brouwer-trees?
The Setting I'm trying to use Agda's well-founded ordering to prove that something is terminating using Brouwer Trees i.e. ...