Re: [isabelle] Bound variables in Code_Evaluation.term

Hi Andreas,

> I am trying to understand how the term representation in Code_Evaluation
> deals with variables.
> The pseudo-constructors Const, App and Abs clearly model constants,
> application and abstraction, but I am having difficulties with the
> purpose of Free. Is Free supposed to model both bound and free variables?
> For example, how is the Isabelle term "x (%x :: nat. x)" to be
> represented in Code_Evaluation? Omitting the types, I came up with the
> following.
>   App (Free x ...) (Abs "x" ... (Free x ...))
> However, it seems strange that the second occurrence of Free actually
> denotes a bound variable. Is that intended?

the classical code evaluation (code_evaluation.ML and particularly
HOLogic.reflect_term) do not cover variables at all.  This is an
extensions of quickcheck narrowing.  You might start your investigation
there (grep -rIFn Code_Evaluation.Free .).

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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