From 719cb8ec4a32382977e48f5f394461b614a2ffbe Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Thu, 22 Aug 2024 09:57:05 +0200 Subject: [PATCH] coq: add value requirement in E-App2 --- coq/smallstep.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/coq/smallstep.v b/coq/smallstep.v index 067678c..63f1cc1 100644 --- a/coq/smallstep.v +++ b/coq/smallstep.v @@ -52,9 +52,10 @@ Inductive beta_step : expr_term -> expr_term -> Prop := e1 -->β e1' -> (expr_app e1 e2) -->β (expr_app e1' e2) - | E_App2 : forall e1 e2 e2', + | E_App2 : forall v1 e2 e2', + (is_value v1) -> e2 -->β e2' -> - (expr_app e1 e2) -->β (expr_app e1 e2') + (expr_app v1 e2) -->β (expr_app v1 e2') | E_TypApp : forall e e' τ, e -->β e' ->