pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-12-01 00:26:18 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Revising for tomorrow's lecture

Browse source
This commit is contained in:
Adam Chlipala 2022-03-13 18:10:19 -04:00
parent f3211734b9
commit c5a69b6253
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
LambdaCalculusAndTypeSoundness.v
View file

@ -312,7 +312,7 @@ Module Ulc.
(* Function application (called "beta reduction") is the big rule here. *) (* Function application (called "beta reduction") is the big rule here. *)
Inductive step : exp -> exp -> Prop := Inductive step : exp -> exp -> Prop :=
| ContextBeta : forall x e v, | Beta : forall x e v,
value v value v
-> step (App (Abs x e) v) (subst v x e) -> step (App (Abs x e) v) (subst v x e)

2
LambdaCalculusAndTypeSoundness_template.v
View file

@ -279,7 +279,7 @@ Module Ulc.
(** * Small-step semantics *) (** * Small-step semantics *)
Inductive step : exp -> exp -> Prop := Inductive step : exp -> exp -> Prop :=
| ContextBeta : forall x e v, | Beta : forall x e v,
value v value v
-> step (App (Abs x e) v) (subst v x e) -> step (App (Abs x e) v) (subst v x e)