The purpose of #evaluateIn: is to transform evrything to Z3 ASTs after we have all the necessary constants in γ. This means that here, expr will evaluateIn: to either a Z3 FuncDecl, or a NaturalTransformation whose components are Z3 FuncDecls. In either case EApp>>evaluateIn: must return the resulting Z3_APP_AST. This is alway possible now after #218.
Without this fix, it was impossible to typecheck annotations containing applications of user-defined functions. For example, in L₈ sumGauss, thm_sum's refined type contains (sum value: m).
The purpose of #evaluateIn: is to transform evrything to Z3 ASTs after we have all the necessary constants in γ. This means that here, expr will evaluateIn: to either a Z3 FuncDecl, or a NaturalTransformation whose components are Z3 FuncDecls. In either case EApp>>evaluateIn: must return the resulting Z3_APP_AST. This is alway possible now after #218.
Without this fix, it was impossible to typecheck annotations containing applications of user-defined functions. For example, in L₈ sumGauss, thm_sum's refined type contains (sum value: m).