Library MetaCoq.Erasure.EWndEval
1-step non-deterministic weak reduction
Section
Wnd
.
Context
(
Σ
:
global_declarations
).
Inductive
Wnd
:
term
→
term
→
Prop
:=
Constant unfolding
|
wConst
c
decl
body
(
isdecl
:
declared_constant
Σ
c
decl
):
decl
.(
cst_body
)
=
Some
body
→
Wnd
(
tConst
c
)
body
Beta
|
wBeta
na
a
b
:
Wnd
(
tApp
(
tLambda
na
b
)
a
) (
subst10
a
b
)
Let
|
wLet
na
b0
b1
:
Wnd
(
tLetIn
na
b0
b1
) (
subst10
b0
b1
).
End
Wnd
.