|
|
|---|
|
|
|
|---|
Check if a binding expression is statically well-formed.
(check-bind-expression vars value body expr ctxt) → result
First we align the variables and the expressions, which also ensures that there is at least one variable. We also ensure that there are no duplicate variable names. We check the static semantics of the expression bound to the variables, and we check whether its types match the variable types, which may generate proof obligations. We augment the context with the binding, and we check the body in this augmented context.