Re: [isabelle] check phases
On Fri, 1 Aug 2014, Lars Noschinski wrote:
The check phase is meant to subsume a variety of mechanisms in the
manner of "type-inference" or "type-reconstruction" or
"type-improvement", not just type-checking in the narrow sense.
By the latter sentence, modifying types and type constraints is
obviously in the scope of check.
Yes, type constraints and certain change of status of type variables is
possible, and actually the main purpose of certain check phases. The
implementation manual has some general explanations on the implicit
polymorphism of terms that apply here as well.
In other situations, term checks perform some kind of higher-order
rewriting. This might include alpha-beta-eta conversions, although within
the syntax one needs to be more careful than within the logic, to avoid
too much user-confusion. Tool confusion is a different thing: in full
generality, the mix of check phases might not work out at all.
Similarly (but not mentioned), the "_" will be replaced by a Var,
capturing all available bounds.
That is some special trickery with "dummy_pattern" -- probably not
something to try at home.
This archive was generated by a fusion of
Pipermail (Mailman edition) and