[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 MHonArc.