syntaxAlchemist/ladder-calculus
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

coq: add value requirement in E-App2

Browse source
This commit is contained in:
Michael Sippel 2024-08-22 09:57:05 +02:00
parent 9c17e9e642
commit 719cb8ec4a
Signed by: senvas
GPG key ID: F96CF119C34B64A6
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
coq/smallstep.v
View file

@ -52,9 +52,10 @@ Inductive beta_step : expr_term -> expr_term -> Prop :=
e1 -->β e1' -> e1 -->β e1' ->
(expr_app e1 e2) -->β (expr_app e1' e2) (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' -> e2 -->β e2' ->
(expr_app e1 e2) -->β (expr_app e1 e2') (expr_app v1 e2) -->β (expr_app v1 e2')
| E_TypApp : forall e e' τ, | E_TypApp : forall e e' τ,
e -->β e' -> e -->β e' ->