defining types

Stream: lean4

[Kayla Thomas]

Is there a simpler way to define VarName here so that Lean still differentiates it as its own type separate from PredName and DefName when they are defined in the same manner? That is, I want to get an error when a term of one of VarName, PredName or DefName is used where it is supposed to be one of the other, and this works, but I am wondering if there is a simpler way.

inductive VarName : Type
  | mk : String → VarName
  deriving Inhabited, DecidableEq

def VarName.toString : VarName → String
  | VarName.mk x => x

instance : ToString VarName :=
  { toString := fun x => x.toString }

instance : Repr VarName :=
  { reprPrec := fun x _ => x.toString.toFormat }

I tried

def VarName : Type := String
  deriving Inhabited, DecidableEq

but it didn't complain when I used a term of

def DefName : Type := String
  deriving Inhabited, DecidableEq

where one of VarName was expected.

[Mac Malone]

@Kayla Thomas Afaik, your approach here is the standard way to achieve that with one caveat: the standard style is to use a structure rather than an inductive. For example:

structure VarName where
  toString : String
  deriving Inhabited, DecidableEq

Also, since String is a structure itself, one can also just do:

structure VarName extends String
  deriving Inhabited, DecidableEq

which has the advantage of giving you all of the dot notation of String for VarName for free.

[Kayla Thomas]

That is much simpler. Thank you!

[Kayla Thomas]

I guess I still need to include the definitions of the instances? If I don't, this gives "failed to synthesize instance ToString VarName" for the eval.

structure VarName extends String
  deriving Inhabited, DecidableEq

#eval [(VarName.mk "a"), (VarName.mk "b")].toString

[Kayla Thomas]

This comes up when I try to define toString for a type that uses these. For example

inductive Formula : Type
  | pred_const_ : PredName → List VarName → Formula

...

def Formula.toString : Formula → String
  | pred_const_ X xs => s! "({X} {xs})"

...

instance : ToString Formula :=
  { toString := fun F => F.toString }

instance : Repr Formula :=
  { reprPrec := fun F _ => F.toString.toFormat }

[Kayla Thomas]

Which is quite ok, I'm just wondering if that is right.

[Mac Malone]

@Kayla Thomas Yeah, that is correct. There does not currently exist a way to automatically derive the instances from the wrapped object.

[Kayla Thomas]

Ok. Thank you.