Re: [isabelle] Bound variables in Code_Evaluation.term
Thanks for the hint to quickcheck narrowing. I now see that Code_Evaluation.Free is only
used to represent uninstantiated terms in counter examples. Abstractions only occur in
quickcheck exhaustive in the special case of dummy abstractions. So there currently is no
need to think about bound variables.
On 18/06/14 22:06, Florian Haftmann wrote:
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
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and