elaborator can't deduce type

Stream: new members

[Shi Zhengyu]

Hi all,
I am wondering why elaborator fail to deduce type in example below. Obviously specify next is of type weekday resolves the type, but I don't find ambiguity without doing so :D

inductive weekday
| monday | tuesday | wednesday | thursday | friday | saturday | sunday
namespace weekday
open weekday (renaming rec -> rec)
def next (d: weekday) := rec tuesday wednesday thursday friday saturday sunday monday d
end weekday

Thanks!

[Kevin Buzzard]

Can you post a #mwe ? I have errors because Lean doesn't know what weekday is.

[Shi Zhengyu]

Kevin Buzzard said:

Can you post a #mwe ? I have errors because Lean doesn't know what weekday is.

editted

[Kevin Buzzard]

This works:

def next (d: weekday) : weekday :=
rec tuesday wednesday thursday friday saturday sunday monday d

as does this:

def next (d: weekday) :=
(rec tuesday wednesday thursday friday saturday sunday monday d : weekday)

Lean was not able to guess the type of the answer without some hints.

[Reid Barton]

It's technically not unambiguous, another possible type is

rec weekday weekday weekday weekday weekday weekday weekday d

and this isn't definitionally equal to weekday.