Models for higher-order function arguments
When verifying Easy/src/LambdaHO.elm
, one does not get a model for the higher-order argument of f
(called HO#f#3
in SMT).
Of course, there is no elm-definition for f
, so this is expected behavior.
But displaying a better reason on why this could not be printed might be a good idea.
So for every function starting with #HO
, something like
"Interpretation of the function f, which is used as a parameter in another function, and therefore can't be displayed. Note: Support for higher-order is very limited"
could be printed instead of
"Interpretation of the function HO#f#3, which is not in the Elm program and therefore can't be displayed."
(which is misleading in this case).
Please note: The number in the naming convention for higher-order arguments is used as a unique identifier and is not part of the variable name in elm.