<div dir="ltr"><div><div><div><div>I get an error that the specified record is recursive.<br></div>I don't understand why it is.</div><div><br></div></div>The code at the moment is full of holes and a bit difficult to read because it is inside a big mutual block.</div><div><br></div><a href="https://github.com/xekoukou/AgdaScript/blob/5fa8728c3c03d33c4b249a1c011958db6e0d36ae/AgdaScript2.agda#L50">https://github.com/xekoukou/AgdaScript/blob/5fa8728c3c03d33c4b249a1c011958db6e0d36ae/AgdaScript2.agda#L50</a><br><br>Removing this line, stops the error from showing up.<br><br><a href="https://github.com/xekoukou/AgdaScript/blob/5fa8728c3c03d33c4b249a1c011958db6e0d36ae/AgdaScript2.agda#L80">https://github.com/xekoukou/AgdaScript/blob/5fa8728c3c03d33c4b249a1c011958db6e0d36ae/AgdaScript2.agda#L80</a><br></div>