<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>