From 6a2f296e32f8daf4ba46cd1a83940385fcd0d283 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Fri, 24 Jul 2020 19:50:20 +0200 Subject: [PATCH] Properties: introduce an implicit argument M for clarity in the type of M-named variables (#454) --- src/plfa/part2/Properties.lagda.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/plfa/part2/Properties.lagda.md b/src/plfa/part2/Properties.lagda.md index 95023b21..e5f9a7cf 100644 --- a/src/plfa/part2/Properties.lagda.md +++ b/src/plfa/part2/Properties.lagda.md @@ -957,11 +957,11 @@ eval : ∀ {L A} → ∅ ⊢ L ⦂ A --------- → Steps L -eval {L} (gas zero) ⊢L = steps (L ∎) out-of-gas +eval {L} (gas zero) ⊢L = steps (L ∎) out-of-gas eval {L} (gas (suc m)) ⊢L with progress ⊢L -... | done VL = steps (L ∎) (done VL) -... | step L—→M with eval (gas m) (preserve ⊢L L—→M) -... | steps M—↠N fin = steps (L —→⟨ L—→M ⟩ M—↠N) fin +... | done VL = steps (L ∎) (done VL) +... | step {M} L—→M with eval (gas m) (preserve ⊢L L—→M) +... | steps M—↠N fin = steps (L —→⟨ L—→M ⟩ M—↠N) fin ``` Let `L` be the name of the term we are reducing, and `⊢L` be the evidence that `L` is well typed. We consider the amount of gas