[isabelle] check phases



Hi,

what transformations are allowed for check phases and which invariants
can I expect to be preserved by check phases? I couldn't find anything
in the implementation manual, but the reference manual at least states
(section 7.5):

    Pre-terms are further processed by the so-called check and uncheck
    phases that are intertwined with type-inference (see also [49]). The
    latter allows to operate on higher-order abstract syntax with proper
    binding an type information already available

(although I'm not sure what "latter" refers to here).

The invariant I am interested in is the preservation of binders: Given a
constant c (declared by myself, so no check-phase should know about it)
and an (unchecked) term t containing c exactly once, then the
Abs(tractions) in t above c are the same as the abstractions above c in
Syntax.check_term ctxt t (of course "same" is a bit fuzzy here --
obviously types and names might change).

Is this a reasonable expectation?



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.