From 643ff85cd09f524cfea8d3378ad30c07cdb8c4dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Fri, 24 Jan 2020 14:59:10 +0100 Subject: [PATCH] =?UTF-8?q?Properties:=20visual=20alignment=20of=20pattern?= =?UTF-8?q?=20matches=20for=20M=20=E2=80=94=E2=86=92=20N=20in=20the=20proo?= =?UTF-8?q?f=20of=20preserve?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/plfa/part2/Properties.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part2/Properties.lagda.md b/src/plfa/part2/Properties.lagda.md index 072368a2..89d8d7eb 100644 --- a/src/plfa/part2/Properties.lagda.md +++ b/src/plfa/part2/Properties.lagda.md @@ -807,7 +807,7 @@ preserve ((⊢ƛ ⊢N) · ⊢V) (β-ƛ VV) = subst ⊢V ⊢N preserve ⊢zero () preserve (⊢suc ⊢M) (ξ-suc M—→M′) = ⊢suc (preserve ⊢M M—→M′) preserve (⊢case ⊢L ⊢M ⊢N) (ξ-case L—→L′) = ⊢case (preserve ⊢L L—→L′) ⊢M ⊢N -preserve (⊢case ⊢zero ⊢M ⊢N) β-zero = ⊢M +preserve (⊢case ⊢zero ⊢M ⊢N) (β-zero) = ⊢M preserve (⊢case (⊢suc ⊢V) ⊢M ⊢N) (β-suc VV) = subst ⊢V ⊢N preserve (⊢μ ⊢M) (β-μ) = subst (⊢μ ⊢M) ⊢M ```