deriving for type definition

Stream: lean4

[James Sully]

Suppose I have something like def FooId := Nat. How do I derive BEq for it? Or do I have to switch to a single field structure?

[Damiano Testa]

This works:

def FooId := Nat
deriving BEq

#synth BEq FooId

[Damiano Testa]

You can also use inferInstanceAs:

def FooId := Nat

instance : BEq FooId := inferInstanceAs (BEq Nat)

#synth BEq FooId

[James Sully]

Thank you!