Questions tagged [termination]
The termination tag has no usage guidance.
5
questions
9
votes
1
answer
172
views
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 ...
- 2,832
6
votes
1
answer
159
views
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 (...
- 5,424
0
votes
1
answer
57
views
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:
...
- 263
5
votes
1
answer
140
views
How to convince Agda that definition is terminating in the presence of unapplied recursion?
In the following, termination check fails for Df:
...
5
votes
1
answer
149
views
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.
...
- 643