|
|
|---|
|
|
|
|---|
Fixtype of pairs consisting of an expression value and a dynamic environment.
This is a product type introduced by fty::defprod.
In general, the execution of an expression not only yields an expression value (see expr-value, but also affects the dynamic environment. Actually, this is not quite the case in the current simple version of Leo, but it will likely be the case when Leo is extended; so we formalize the necessary mathematical structure for right now.