Skip to main content

Questions tagged [positivity]

Positivity is a common restriction when defining inductive types in type-theory based proof assistants.

2 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
5 votes
0 answers
163 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
1 vote
0 answers
60 views

Why does Coq not allow constructor argument types to be strictly positive mutual inductive types?

Note: Apologies for the wicked mouthful of a title. I'm still getting acquainted with Coq terminology, so I might not have chosen the best words. If you have a better title suggestion, edits are more ...
Kyle Lin's user avatar
  • 143