# Re: [isabelle] Basic help with class and instantiation

```On Thu, 16 Aug 2012, Yannick Duchêne (Hibou57) wrote:

```
```I tried to add type annotations everywhere I could, which gave:

class cls1 =
fixes
cls1_x :: "'a" and
cls1_f :: "'a ⇒ 'a" and
cls1_g :: "nat ⇒ 'a"
assumes
cls1_fg_prop: "(cls1_f (cls1_g (0::nat))) = (cls1_g (0::nat))"

fun f :: "int ⇒ int" where
"f (i::int) = (i::int)"

fun g :: "nat ⇒ int" where
"g (n::nat) = (int (n::nat))"

declare [[show_types]] -- Testing
declare [[show_consts]] -- Testing
declare [[show_sorts]] -- Testing

instantiation int :: cls1
begin
definition df: "(cls1_f (i::int)) = (f (i::int))"
definition dg: "(cls1_g (n::nat)) = (g (n::nat))"
instance proof
have "(cls1_f (0::int)) = (f (0::int))" using df by simp -- Testing
have "(cls1_g (0::nat)) = (g (0::nat))" using dg by simp -- Testing
have "(f (g (0::nat))) = (g (0::nat))" by simp
then show "(cls1_f (cls1_g (0::nat))) = (cls1_g (0::nat))"
using df and dg by simp
qed
end
```
```
Try this one:

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

```
The Prover IDE helped to expose the type of cls1_f and cls2_g in the text, using CTRL/COMMAND hover.
```

```
The result is the same. May be that's finally a bug, or else don't see why it can't unify the expression to be shown with the pending goal.
```
```
By the way, is there a recommended way to submit bug reports (if that's really one) about Isabelle?
```
As a rule of thumb there are hardly any bugs, only unexpected behaviour,
and that is best discussed on the mailing list.

Makarius
```

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