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 MHonArc.