Feature that implicit parameters not inferred in `theorem`?

Stream: lean4

[C7X]

Today a difference came up in my code in how implicit parameters are inferred in a term in the statement of a theorem vs. elsewhere, even if they are the same type. I asked in a channel specific to the library I was working on, and I heard that it's likely a design feature of Lean. If it is, which design feature of Lean causes implicit parameters to be inferrable in one place but not in the other?

import Mathlib

def test (a b : ℕ) {c : ℕ → ℕ} : Prop := b = c a

-- Implicit parameters work properly here, `test a b` can see the term of type `ℕ → ℕ` and infer it.
#check ∀ (a b : ℕ), ∀ (_ : ℕ → ℕ), test a b

-- It cannot infer here.
theorem test2 : ∀ (a b : ℕ), ∀ (_ : ℕ → ℕ), test a b := by sorry

[Aaron Liu]

If you hover over the term that #check displays in the infoview I think you'll see that it has not inferred c as the implicit parameter, but instead has just left a metavariable in there

[Aaron Liu]

So the difference isn't that an implicit argument is being inferred, but that #check is allowing you to have a term with unassigned metavariables, but the theorem test2 is not letting you do that

[C7X]

This makes sense, thanks!

[Snir Broshi]

Well Lean does infer stuff from assumptions sometimes:

import Mathlib

def foo1 (l : List ℕ) {hl} := l[5]

theorem foo2 (l : List ℕ) {h₇ h₁₀ h₄} : l[4] + l[10] = l[7] := sorry

It might be specific to the square brackets syntax (docs#GetElem) but I'm not sure

[Aaron Liu]

yeah it's filled in with a tactic