Re: [isabelle] Free variables vs schematic variables



On Wed, Jun 13, 2012 at 12:55 PM, Steve Wong <s.wong.731 at gmail.com> wrote:
> Hi,
>
> Just a quick question: how come Isabelle keeps a distinction between free
> and schematic variables? It seems that free variables in a goal are
> converted to schematic anyway, so what are the benefits of keeping them
> distinct?

How would you propose to fuse the concepts?
Do you mean Isabelle/HOL should use free variables wherever it
currently uses schematic variables, or schematic variables wherever it
currently uses free, or should use something different for both?
Thinking about that question might make it more obvious why there are
two kinds of "free" variable.

(I'm looking forward to an expert's answer, though: as I understand
it, the distinction is fundamentally unavoidable because one kind of
variable is in the object-logic syntax and the other is a meta-logic
variable. But I may be wrong about this.)





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