Skip to main content

Questions tagged [well-founded-induction]

Filter by
Sorted by
Tagged with
0 votes
0 answers
71 views

How to get term describing case of pattern match in Coq

In Coq, While trying to write a definition of a function with well-founded recursion, I found myself wanting/having to reference that a term I was trying to match ...
C.E.Sally's user avatar
  • 121
5 votes
0 answers
166 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): ...
Ilk's user avatar
  • 547
5 votes
1 answer
176 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. ...
Joey Eremondi's user avatar