[Agda] what is the condition for well-formedness of an inductive-recursive definition?

[Jason Hu]

Hi all,

I am trying to understand what constitutes a valid inductive-recursive definition. In particular, I am interested in the syntactic criteria and how Agda checks it. Surely the inductive part must be strictly positive, but what' the condition on the recursive part? It doesn't occur to obvious to me what the recursion can refer to. Can it refer back to the inductive part that is being defined?

Thanks,
Jason Hu
https://hustmphrrr.github.io/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20241015/efd5354f/attachment.html>