Re: [isabelle] Basic help with class and instantiation



Le Thu, 16 Aug 2012 18:45:19 +0200, Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr> a écrit:

On Thu, 16 Aug 2012 16:44:43 +0200, Makarius <makarius at sketis.net> wrote:

Try this one:

   show "(cls1_f (cls1_g (0::nat) :: int)) = (cls1_g (0::nat))"
                                  ^^^^^^

And yes, this solves the unification! (Makarius is a genius :-P )

Any of this three ones do:

   then show "(cls1_f (cls1_g 0)) = ((cls1_g 0) :: int)"
   then show "((cls1_f (cls1_g 0)) :: int) = (cls1_g 0)"
   then show "(cls1_f ((cls1_g 0) :: int)) = (cls1_g 0)"


The case is in the practical way solved, but something still holds mysterious things. With or without the “::int” annotation, at the beginning 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 it deeper a later time.


--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University






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