Re: [isabelle] Comparing polymorphic functions
On Tue, Feb 1, 2011 at 3:18 PM, Makarius <makarius at sketis.net> wrote:
> For the logical framework, schematic variables are arbitrary (can be
> instantiated), while free variables are fixed (local constant that might
> become arbitrary after leaving the scope).
> Type inference has a third category of "parameters" that can get unified in
> the type checking process. There is no user notation for that, apart from
> nameless dummies "_". Otherwise type-inference insists that schematic and
> free variables work out as they are written, no instantiation of schematic
> variables here.
> The above 'schematic_lemma' would give you a chance to instantiate
> schematic variables in the course of reasoning, after type-checking has
> already succeeded. Further confusion might be causes by proof tools that
> choke on schematic type variables in a goal.
If I understand this correctly, schematic variables can be instantiated but
schematic *type* variables cannot due to a restriction of type-inference.
Thus, there's no polymorphism of any kind at the meta-level. Likewise, with
type variables because they are free variables. So it's expected that this
lemma "(x::'a) = (y::'b)"
Because both 'a and 'b are free variables. But this works fine:
x :: 'a
lemma "x = (y::'b)"
Isn't 'a regarded as a free variable? How come it can be instantiated?
This archive was generated by a fusion of
Pipermail (Mailman edition) and