Specifying implicit parameter to `rec_on`

Stream: new members

[Rajiv]

I was experimenting with the weekday example from Theorem Proving with Lean (https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html#enumerated-types), using the following code snippet.

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

#check @weekday.rec_on

-- weekday.rec_on :
--   Π {C : weekday → Sort u_1} (n : weekday),
--     C weekday.sunday →
--     C weekday.monday →
--     C weekday.tuesday →
--     C weekday.wednesday →
--     C weekday.thursday →
--     C weekday.friday →
--     C weekday.saturday →
--     C n

-- For all functions C from weekday to types, all terms n of type
-- weekday, if you have a term C weekday.sunday, and a term C
-- weekday.monday, ..., and a term C weekday.saturday, then I can give
-- you a term of type C n. In addition, I'll also try to infer the
-- function C.

def number_of_day (d : weekday) : ℕ :=
  weekday.rec_on d 1 2 3 4 5 6 7

#check (λ _ : weekday, ℕ)

def number_of_day₁ (d : weekday) : ℕ :=
  weekday.rec_on (λ _ : weekday, ℕ) d 1 2 3 4 5 6 7

In number_of_day₁ function, when I explicitly try to give the lambda for function C, it throws an error. I was wondering why that is so?

[Kevin Buzzard]

Because the input {C : weekday → Sort u_1} means "Lean will figure out this term from the types of all the other terms you give it". If you want to explicitly supply this parameter C you can do it with @weekday.rec_on , which means that the user then has to supply all the inputs to the function.

[Rajiv]

Thanks again, Prof Kevin. That works!