<div dir="ltr">Hi,<br><br>I'm (slowly) working through Philip Wadler's PLFA course.<br><div>I happen to be using Agda 2.6.1, from the git 'master' branch at commit d8449caf816e0c5e13419ee2d3fe32a047ec3db8,</div><div>and I ran into a termination checking failure in the 'eval' function in the Properties.lagda chapter.<br></div><br>This version (from the text)<br><br><div style="margin-left:40px"><span style="font-family:courier new,monospace">eval : âˆ€ {L A}<br>  â†’ Gas<br>  â†’ âˆ… âŠ¢ L â¦‚ A<br>  Â  ---------<br>  â†’ Steps L<br>eval {L} (gas zero) Â  Â âŠ¢L Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  = Â steps (L âˆŽ) out-of-gas<br>eval {L} (gas (suc m)) âŠ¢L with progress âŠ¢L<br>... | done VL Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  = Â steps (L âˆŽ) (done VL)<br>... | step L—→M with eval (gas m) (preserve âŠ¢L L—→M)<br>... Â  Â | steps M—↠N fin Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  = Â steps (L â€”→⟨ L—→M âŸ© M—↠N) fin</span></div><span style="font-family:courier new,monospace"></span><div><br></div><div>fails termination checking.  Note that 'Gas' is just a type that holds a natural number:</div><div><br></div><div style="margin-left:40px">data Gas : Set where<br>  gas : â„• â†’ Gas</div><div><br></div><div>However, if one just replaces Gas with â„• in the function, the termination checker is happy:</div><div><br></div><div style="margin-left:40px">eval : âˆ€ {L A}<br>  â†’ â„•<br>  â†’ âˆ… âŠ¢ L â¦‚ A<br>  Â  ---------<br>  â†’ Steps L<br>eval {L} zero Â  Â âŠ¢L Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  = Â steps (L âˆŽ) out-of-gas<br>eval {L} (suc m) âŠ¢L with progress âŠ¢L<br>... | done VL Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  = Â steps (L âˆŽ) (done VL)<br>... | step L—→M with eval m (preserve âŠ¢L L—→M)<br>... Â  Â | steps M—↠N fin Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  = Â steps (L â€”→⟨ L—→M âŸ© M—↠N) fin</div><div><br></div><div>Is this an intentional change in the termination checking?</div><div><br></div><div>- Dan</div><div><br></div></div>