pub fn fill_defaults<'t>(
surface: &Surface,
term: Cow<'t, Term>,
) -> Cow<'t, Term>Expand description
Fill every OMITTED DEFAULT ARGUMENT in term, at every application spine in it.
★ THIS IS THE SECOND HALF OF THE SAME STAGING resolve_names IS THE FIRST HALF OF. Lean’s
order is: resolve what the names denote, expand what the spellings abbreviate, and only then
hand a term to the elaborator — which is why the kernel needs to know nothing about either.
withDefault 1 is a SPELLING of withDefault 1 3, exactly as token inside open Alpha is a
spelling of Alpha.token, so it is expanded here rather than being taught to the elaborator as
a fourth kind of argument insertion.
A BARE NAME IS NOT A CALL SITE. Check withDefault. reports the function, and
Definition g : Int -> Int := withDefault. is the function it already was — Lean answers both
the same way, and filling a default into a term nobody applied would change what an unapplied
constant MEANS. Filling stops at the first parameter with no default, which is what makes the
trailing-position rule positional: f 1 against (a) (m := 3) (b) becomes f 1 3, still
awaiting b.
Takes and returns a Cow so it composes directly onto resolve_names’s result: a term that
omits no default costs one read-only walk, and a session that declared no default at all costs
not even that (Surface::fills_defaults).