michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Properties: introduce an implicit argument M for clarity in the type of M-named variables (#454)

Browse source
This commit is contained in:
Marko Dimjašević 2020-07-24 19:50:20 +02:00 committed by GitHub
parent 4e40ef4ab3
commit 6a2f296e32
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/plfa/part2/Properties.lagda.md
View file

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