Re: [isabelle] Printing instantiations



Hi Florian,

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
> be
> > 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.

Thanks,
Steve


> Hope this helps,
>        Florian
>
> --
>
> Home:
> http://www.in.tum.de/~haftmann
>
> PGP available:
>
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>
>




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