Making inductive type instance of has_repr type class

Stream: new members

[Mukesh Tiwari]

Could some one please tell me what is wrong with my code. I have defined a inductive type and trying to make it instance of has_repr, but getting this error "equation compiler error, equation #2 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable"

inductive day : Type
| monday : day
| tuesday : day
| wednesday : day
| thursday : day
| friday : day
| saturday : day
| sunday : day

protected def day.repr : day → string
| monday  := "monday"
| tuesday := "tuesday"
| wednesday := "wednesday"
| thursday := "thursday"
| friday := "friday"
| saturday := "saturday"
| sunday := "sunday"


instance : has_repr day :=
(day.repr)

[Joe]

Put everything into the namespace day

inductive day : Type
| monday : day
| tuesday : day
| wednesday : day
| thursday : day
| friday : day
| saturday : day
| sunday : day

namespace day

protected def repr : day → string
| monday  := "monday"
| tuesday := "tuesday"
| wednesday := "wednesday"
| thursday := "thursday"
| friday := "friday"
| saturday := "saturday"
| sunday := "sunday"

instance : has_repr day :=
⟨day.repr⟩

end day

[Joe]

or open day before your definition of day.repr

[Mukesh Tiwari]

@Joe Thank you very much. I also noticed that my brackets were ( instead of ⟨.

[Joe]

You are welcome.

[Kenny Lau]

inductive day : Type
| monday : day
| tuesday : day
| wednesday : day
| thursday : day
| friday : day
| saturday : day
| sunday : day

protected def day.repr : day → string
| day.monday  := "monday"
| day.tuesday := "tuesday"
| day.wednesday := "wednesday"
| day.thursday := "thursday"
| day.friday := "friday"
| day.saturday := "saturday"
| day.sunday := "sunday"

instance : has_repr day :=
⟨day.repr⟩

[Kenny Lau]

if you use monday instead of day.monday, Lean treats that as a variable

[Kenny Lau]

so it's as if you wrote:

inductive day : Type
| monday : day
| tuesday : day
| wednesday : day
| thursday : day
| friday : day
| saturday : day
| sunday : day

protected def day.repr : day → string
| x  := "monday"

instance : has_repr day :=
⟨day.repr⟩

[Kenny Lau]

and that's why the second equation would never be used