*To*: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>*Subject*: Re: [isabelle] Basic help with class and instantiation*From*: Makarius <makarius at sketis.net>*Date*: Sat, 18 Aug 2012 21:14:56 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <op.wi67tqqbule2fv@douda-yannick>*References*: <op.wiz568nrule2fv@douda-yannick> <op.wi4j9voqule2fv@douda-yannick> <502CB0B2.7040509@informatik.tu-muenchen.de> <op.wi4zq9zzule2fv@douda-yannick> <op.wi47htqmule2fv@douda-yannick> <op.wi67tqqbule2fv@douda-yannick>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Fri, 17 Aug 2012, Yannick Duchêne (Hibou57) wrote:

The case is in the practical way solved, but something still holdsmysterious things. With or without the “::int” annotation, at thebeginning of the proof, there was this:proof (state): step 1 goal (1 subgoal): 1. cls1_f (cls1_g (0∷nat)) = cls1_g (0∷nat) constants: […] cls1_g :: nat ⇒ int cls1_f :: int ⇒ int […]Types are correctly inferred at the beginning, but later forgotten?That's strange. I will stay with this for now, but wish to understand itdeeper a later time.

Makarius

**References**:**[isabelle] Basic help with class and instantiation***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Basic help with class and instantiation***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Basic help with class and instantiation***From:*Florian Haftmann

**Re: [isabelle] Basic help with class and instantiation***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Basic help with class and instantiation***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Basic help with class and instantiation***From:*Yannick Duchêne (Hibou57)

- Previous by Date: Re: [isabelle] Basic help with class and instantiation
- Next by Date: [isabelle] Postdoctoral Opening at the University of Minnesota
- Previous by Thread: Re: [isabelle] Basic help with class and instantiation
- Next by Thread: Re: [isabelle] Basic help with class and instantiation
- Cl-isabelle-users August 2012 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