constant type class instance

Stream: new members

[Drew Moore]

Is there a way to declare constant instances? The line #check below raises 'failed to synthesize type class instance ...'

variables (B: Type) (b: B)
instance B_inhabited: inhabited B :=
⟨ b ⟩
#check default B

[Bryan Gin-ge Chen]

There can't be an inhabited B instance for arbitrary B : Type though. What if B = empty?

[Drew Moore]

Ah that makes sense. I'm just trying to learn type classes in Lean, and would like to use examples like one would create with constant. Initially, I used constants, but that also complains, but because of 'noncomputability'.

constants (B: Type) (b: B)
instance B_inhabited: inhabited B :=
⟨ b ⟩
#check default B

[Bryan Gin-ge Chen]

You can do this:

constants (B: Type) (b: B)
noncomputable instance B_inhabited: inhabited B :=
⟨ b ⟩
#check default B

or

constants (B: Type) (b: B)
noncomputable theory
instance B_inhabited: inhabited B :=
⟨ b ⟩
#check default B

[Drew Moore]

thank you!