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

More: fixes the syntax of substitution in a wrong translation of case× (#532)

Browse source 
* More: fixes the syntax of substitution in a wrong translation of case×

* More: fixes the names of projection functions in an intentionally wrong translation
This commit is contained in:
Marko Dimjašević 2020-10-24 17:04:30 +02:00 committed by GitHub
parent 753029e3ad
commit a9ecf866c2
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/More.lagda.md
View file

@ -271,14 +271,14 @@ One might think that we could instead use a more compact translation:
-- WRONG
(case× L [⟨ x , y ⟩⇒ N ]) †
=
(N †) [ x := proj₁ (L †) ][ y := proj₂ (L †) ]
(N †) [ x := `proj₁ (L †) ] [ y := `proj₂ (L †) ]
But this behaves differently. The first term always reduces `L`
before `N`, and it computes `proj₁` and `proj₂` exactly once. The
before `N`, and it computes ```proj₁`` and ```proj₂`` exactly once. The
second term does not reduce `L` to a value before reducing `N`, and
depending on how many times and where `x` and `y` appear in `N`, it
may reduce `L` many times or not at all, and it may compute `proj₁`
and `proj₂` many times or not at all.
may reduce `L` many times or not at all, and it may compute ```proj₁``
and ```proj₂`` many times or not at all.
We can also translate back the other way: