Partial Typeclasses?

Stream: lean4

[Andrés Goens]

Is there a way to define a typeclass instance that might be inferred on some cases but not necessarily others (and let Lean complain in those other cases that it can't)? Conceretely, imagine I have a type

abbrev Positive := { x : Nat // x > 0 }

I can define an OfNat instance for Positive for everything except 0. I could do something like:

instance {n : Nat} (h : n ≠ 0) : OfNat Positive n where
  ofNat := ⟨n, (by cases n <;> aesop )⟩

but that won't work then if I somewhere later try to use a positive number where I need it to be Positive, e.g.

example : Positive := 1 -- failed to synthesize instance  OfNat Positive 1

Is there a way to get that last one to work? Particularly for OfNat where the typeclass is specifically defined on the actual values, I would expect that to be possible somehow?

[Eric Wieser]

For this particular case you can use [NeZero n] in place of h

[Andrés Goens]

ah, that's an interesting idea! use another typeclass for the property. It does work for me for this case, but I don't understand how I would define the typeclass instance NeZero for all n : Nat except 0 (and in this case it seems to be burried under a lot of mathlib magic)

[Mario Carneiro]

you could have an instance for NeZero (n+1)