Description
Maybe it's worth considering reconciling all the relational hierarchy at each arity wrt definitions of:
Irrelevant
Recomputable
Stable
WeaklyDecidable
Decidable
Satisfiable
Empty
Universal
etc. (the list may grow...)
because otherwise, we have a lot of redundant repetition on the one hand, but with 'gaps' on the other. There's some overlap/degeneracy at arity 0 for eg Satisfiable
/Universal
(the identity) and Empty
(negation), but I think that is harmless...
Maybe there are good reasons to do with dependencies (eg. Relation.Nullary.Decidable.Core.recompute
can't be typed with a Nullary
definition of Recomputable
... unless we bite the bullet and lift it out into a Relation.Nullary.Definitions
etc. But maybe that's not such a bad idea, either? See also #2243 for my current approach to this particular predicate...
UPDATED: partial fix in #2259 (and largely orthogonal to #2243 )
Activity
Relation.Nullary.Decidable
#2059Acc
essible elements of)WellFounded
relations #2126Relation.Nullary.Recomputable
plus consequences #2243fixes agda#2091
Systematise relational definitions at all arities (#2259)
jamesmckinna commentedon Feb 5, 2024
Reconsidering whether to keep this open, I think on balance after the merge of #2259 that this one can be considered closed by that PR... the other cases being a little too non-uniform to be worth pursuing?
Systematise relational definitions at all arities (#2259)
Merge v2.1.1 into `master` (#2473)