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

Merge branch 'dev' of https://github.com/plfa/plfa.github.io into dev

Browse source
This commit is contained in:
wadler 2018-10-14 11:57:14 +01:00
commit a934950066
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/plfa/Lambda.lagda
View file

@ -236,14 +236,14 @@ Write out the definition of multiplication in the same style.
### Formal vs informal
In informal presentation of formal semantics, one uses choice of
variable name to disambiguate and writes `x` rather than `` x`
variable name to disambiguate and writes `x` rather than `` ` x ``
for a term that is a variable. Agda requires we distinguish.
Similarly, informal presentation often use the same notation for
function types, lambda abstraction, and function application in both
the object language (the language one is describing) and the
meta-language (the language in which the description is written),
trusting readers can use context to distinguish the two. Agda is is
trusting readers can use context to distinguish the two. Agda is
not quite so forgiving, so here we use `ƛ x ⇒ N` and `L · M` for the
object language, as compared to `λ x → N` and `L M` in our
meta-language, Agda.