From c5a69b6253ad2aa9260da6ee797196c428b847b2 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 13 Mar 2022 18:10:19 -0400 Subject: [PATCH] Revising for tomorrow's lecture --- LambdaCalculusAndTypeSoundness.v | 2 +- LambdaCalculusAndTypeSoundness_template.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/LambdaCalculusAndTypeSoundness.v b/LambdaCalculusAndTypeSoundness.v index 05a2adf..66e9c20 100644 --- a/LambdaCalculusAndTypeSoundness.v +++ b/LambdaCalculusAndTypeSoundness.v @@ -312,7 +312,7 @@ Module Ulc. (* Function application (called "beta reduction") is the big rule here. *) Inductive step : exp -> exp -> Prop := - | ContextBeta : forall x e v, + | Beta : forall x e v, value v -> step (App (Abs x e) v) (subst v x e) diff --git a/LambdaCalculusAndTypeSoundness_template.v b/LambdaCalculusAndTypeSoundness_template.v index ef200c1..8950521 100644 --- a/LambdaCalculusAndTypeSoundness_template.v +++ b/LambdaCalculusAndTypeSoundness_template.v @@ -279,7 +279,7 @@ Module Ulc. (** * Small-step semantics *) Inductive step : exp -> exp -> Prop := - | ContextBeta : forall x e v, + | Beta : forall x e v, value v -> step (App (Abs x e) v) (subst v x e)