All Questions
2
questions
3
votes
1
answer
391
views
How to provide proof for termination in Agda?
I am trying to write an integer division function from scratch in agda2 (as of 2.6.3):
...
- 2,220
5
votes
1
answer
177
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.
...
- 921