[isabelle] check phases
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
Pre-terms are further processed by the so-called check and uncheck
phases that are intertwined with type-inference (see also ). 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