Zulip Chat Archive

Stream: new members

Topic: constant type class instance


view this post on Zulip Drew Moore (Jun 28 2020 at 00:32):

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

view this post on Zulip Bryan Gin-ge Chen (Jun 28 2020 at 00:37):

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

view this post on Zulip Drew Moore (Jun 28 2020 at 00:41):

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

view this post on Zulip Bryan Gin-ge Chen (Jun 28 2020 at 00:42):

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

view this post on Zulip Drew Moore (Jun 28 2020 at 00:42):

thank you!


Last updated: May 14 2021 at 00:42 UTC