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