[isabelle] Bound variables in Code_Evaluation.term
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and