From 3673bc8d26dd1ce900d3b75a17af0e7fa3281512 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Sun, 7 Jun 2020 22:38:34 +0200 Subject: [PATCH] Lambda: fix highlighting of bindings in the text --- src/plfa/part2/Lambda.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plfa/part2/Lambda.lagda.md b/src/plfa/part2/Lambda.lagda.md index 08798dc3..a5aceba8 100644 --- a/src/plfa/part2/Lambda.lagda.md +++ b/src/plfa/part2/Lambda.lagda.md @@ -1236,8 +1236,8 @@ to use them inside other binding contexts as well as at the top level. Here the two lookup judgments `∋m` and `∋m′` refer to two different bindings of variables named `"m"`. In contrast, the two judgments `∋n` and `∋n′` both refer to the same binding of `"n"` but accessed in different -contexts, the first where "n" is the last binding in the context, and -the second after "m" is bound in the successor branch of the case. +contexts, the first where `"n"` is the last binding in the context, and +the second after `"m"` is bound in the successor branch of the case. And here are typings for the remainder of the Church example: ```