Defining a motive

Stream: new members

[Golden]

Hello all,
I'm a bit confused about how motive is being specified although it is an implicit parameter.

universe u

inductive list (α : Type u) where
  | nil  : list α
  | cons : α → list α → list α

namespace list

def append {α : Type u} (as bs : list α) : list α :=
  match as with
  | nil       => bs
  | cons a as => cons a (append as bs)

theorem nil_append {α : Type u} (as : list α) : append nil as = as :=
  rfl

theorem cons_append {α : Type u} (a : α) (as bs : list α)
                    : append (cons a as) bs = cons a (append as bs) :=
  rfl

theorem append_nil {α : Type u} (as : list α) : append as nil = as :=
  list.rec (motive := fun b => append b nil = b)
    (show append nil nil = nil from rfl)
    (fun (a : α) (as : list α) (ih : append as nil = as) =>
      show append (cons a as) nil = (cons a as) from
      calc append (cons a as) nil
        _ = cons a (append as nil) := rfl
        _ = cons a as := by rw [ih])
    as

@list.rec : {α : Type u_2} →
  {motive : list α → Sort u_1} →
    motive list.nil → ((a : α) → (a_1 : list α) → motive a_1 → motive (list.cons a a_1)) → (t : list α) → motive t

What I am led to believe is that

(motive := ...)

is being used to specify the explicitly define the motive, overriding lean trying to infer what motive is, but I've never seen this syntax used before?
In a sense, it reminds me of

let motive := ...

Am I right in thinking this, or is there actually a different reason for this?

[Edward van de Meent]

f (a := b) is notation to specify the value b for fs implicit parameter named a