Zulip Chat Archive

Stream: new members

Topic: Making inductive type instance of has_repr type class


view this post on Zulip Mukesh Tiwari (Dec 30 2019 at 02:11):

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)

view this post on Zulip Joe (Dec 30 2019 at 02:19):

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

view this post on Zulip Joe (Dec 30 2019 at 02:20):

or open day before your definition of day.repr

view this post on Zulip Mukesh Tiwari (Dec 30 2019 at 02:26):

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

view this post on Zulip Joe (Dec 30 2019 at 02:27):

You are welcome.

view this post on Zulip Kenny Lau (Dec 30 2019 at 03:33):

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

view this post on Zulip Kenny Lau (Dec 30 2019 at 03:34):

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

view this post on Zulip Kenny Lau (Dec 30 2019 at 03:34):

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

view this post on Zulip Kenny Lau (Dec 30 2019 at 03:34):

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


Last updated: May 15 2021 at 23:13 UTC