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)
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
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and