Re: [isabelle] Printing instantiations
On Mon, Jun 21, 2010 at 7:55 AM, Florian Haftmann <
florian.haftmann at informatik.tu-muenchen.de> wrote:
> This looks not so beautiful but in practice such chained existential
> introduction would be accomplished e.g. by blast.
> The details can be found in the tutorial, chapter "The rules of the game".
Thanks. Your explanation is very helpful.
> > But doesn't Isabelle support polymorphism? If so, types shouldn't need to
> > explicitly declared, right?
> These are two different things: polymorphism vs. type inference. Type
> inference assigns most general types, which may be more general than
> actually wanted.
I see. Are there other ways to prevent type inference from assigning types
more general than wanted beside explicitly giving F a specific type?
Ideally, I'd like to existentially quantify over the type of F (and x), but
I think Isabelle/HOL doesn't support quantification over types.
> Hope this helps,
> PGP available:
This archive was generated by a fusion of
Pipermail (Mailman edition) and