
<html>

<head>

<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">

<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>

</head>

<body dir="ltr">

<div class="elementToProof" style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">

Hi all,</div>

<div id="Signature" class="elementToProof">

<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">

<br>

</div>

<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">

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?</div>

<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">

<br>

</div>

<div style="direction: ltr; font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 16px; color: rgb(0, 0, 0);">

<b>Thanks,</b></div>

<div style="direction: ltr; font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 16px; color: rgb(0, 0, 0);">

<b>Jason Hu</b></div>

<div style="direction: ltr; font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">

<span style="font-size: 16px;"><b><a href="https://hustmphrrr.github.io/" id="OWAbe491b0c-fadc-2d66-512a-036e3c38edff" class="OWAAutoLink">https://hustmphrrr.github.io/</a></b></span><br>

</div>

</div>

</body>

</html>