All Questions
Tagged with agda well-founded-induction
2
questions
5
votes
0
answers
168
views
What are the conditions for Agda to detect that induction-recursion has a least fixed point?
This is a 3rd in a series of questions, spurred by my attempts to encode an argument by Danielsson [1] [2] regarding existence of syntactically non-strictly positive datatype.
The idea (rephrased):
...
- 547
5
votes
1
answer
178
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.
...
- 971