in a recursive definition, the recursive call must specify the arguments before the colon

[kim-em]

In Lean 3, when making a recursive definition using the equation compiler, you had to leave out arguments that came before the colon when making a recursive call. In Lean 4, these arguments are required.

e.g. we used to write (from Lean 3 core)

instance decidable_mem [decidable_eq α] (a : α) : ∀ (l : list α), decidable (a ∈ l)
| []     := is_false not_false
| (b::l) :=
  if h₁ : a = b then is_true (or.inl h₁)
  else match decidable_mem l with
  | is_true  h₂ := is_true (or.inr h₂)
  | is_false h₂ := is_false (not_or h₁ h₂)
  end

but now write (from mathlib4):

instance decidableMem [DecidableEq α] (a : α) : ∀ (l : List α), Decidable (a ∈ l)
  | []     => isFalse not_false
  | b :: l =>
    if h₁ : a = b then isTrue (Or.inl h₁)
    else match decidableMem a l with
      | isTrue h₂  => isTrue (Or.inr h₂)
      | isFalse h₂ => isFalse (not_or_intro h₁ h₂)

mathport will need to insert these additional arguments while translating.

See e.g. https://github.com/leanprover-community/mathlib3port/blob/d82ba1c/Mathbin/Data/List/Defs.lean#L39.