From 2644878f94fc44b24049dfbbaddc8f4c03323399 Mon Sep 17 00:00:00 2001 From: phi16 Date: Sun, 14 Oct 2018 04:04:46 +0900 Subject: [PATCH] Fix code highlighting, typo --- src/plfa/Lambda.lagda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plfa/Lambda.lagda b/src/plfa/Lambda.lagda index 7363f465..02fe4ec3 100644 --- a/src/plfa/Lambda.lagda +++ b/src/plfa/Lambda.lagda @@ -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.