*To*: Peter Lammich <lammich at in.tum.de>*Subject*: Re: [isabelle] Isar polymorphism problem*From*: Makarius <makarius at sketis.net>*Date*: Mon, 28 Apr 2014 20:36:37 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk, Ed Schwartz <edmcman at gmail.com>*In-reply-to*: <1398699339.2438.83.camel@lapbroy33>*References*: <CAHPz_Mr8KgKU4966DTROET1AgtJs-gDfU-YQ=AVNZUzcDRxz6Q@mail.gmail.com> <1398688712.2438.74.camel@lapbroy33> <CAHPz_Mq6WGbEq4KrdMdH9NDSJt7-0foS02-R13s0fji1OfPcQw@mail.gmail.com> <1398699339.2438.83.camel@lapbroy33>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Mon, 28 Apr 2014, Peter Lammich wrote:

You can prove the statement \<exists>f::'a1 => ... => 'an => 'b. P f However, in the proof you cannot make any additional assumptions about the type variables, in particular you cannot instantiate them.The only way in Isabelle/HOL to express types with certain propertiesare type-classes, which have several restrictions, e.g., they can onlydepend on one type variable.

Makarius

**References**:**[isabelle] Isar polymorphism problem***From:*Edward Schwartz

**Re: [isabelle] Isar polymorphism problem***From:*Peter Lammich

**Re: [isabelle] Isar polymorphism problem***From:*Peter Lammich

- Previous by Date: Re: [isabelle] Excluding theories from the session_graph output
- Next by Date: Re: [isabelle] Excluding theories from the session_graph output
- Previous by Thread: Re: [isabelle] Isar polymorphism problem
- Next by Thread: [isabelle] Final CFP - Joint Automated Reasoning Workshop & Deduktionstreffen
- Cl-isabelle-users April 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list