Hi

I must be missing something, but I do not understand why the following fails (tested with Coq.8.13.2):

```
Class Inhabited (A : Type) := { inh : A }.
Instance unit_Inhabited : Inhabited unit := { inh := tt }.
Section prod.
Generalizable Variables A B.
Context `{EA : Inhabited A, EB : Inhabited B}.
Instance prod_Inhabited : Inhabited (A*B) :=
{ inh := (inh, inh) }.
End prod.
Lemma dummy {A:Type} `{HA : Inhabited A} : A.
Proof. exact inh. Qed.
Lemma ok : unit.
Proof. apply dummy. Qed.
Lemma ko : unit * unit.
Proof. Fail apply dummy. Abort.
```

Thanks!

You need to reexport the instance: `Existing Instance prod_Inhabited.`

Thanks, it works! But what does it mean?

instance in section is local by default

If you use `Instance`

inside `Section`

, the instance only lives as long as the section. Outside, it is just a plain definition. So, you can register it again using `Existing Instance`

.

Ok, thanks a lot. Maybe the documentation could explain it in the section "Sections and contexts" ;-) Actually now I understand the meaning of `#[global]`

, which I guess does the same?

I have another question regarding typeclasses: can the mechanism be called by hand, if I have e.g. such a goal:

```
Lemma test : Inhabited (unit * unit).
```

?

`typeclasses eauto`

should do the trick.

Or `exact _`

.

Great, many thanks!

Last updated: Oct 03 2023 at 04:02 UTC