Unexpected behaviour of specifying implicit arguments

Stream: lean4

[Kenny Lau]

Just an interesting observation here, that somehow (n := n) works even outside the "scope" of DFunLike.coe in the second example

import Mathlib

axiom A : Type
@[instance] axiom funlikeA : FunLike A Nat Nat
axiom f {n : Nat} : A

variable (m n : Nat)

#check f (n := n) m -- @DFunLike.coe A Nat (fun x => Nat) funlikeA (@f n) m
#check f m (n := n) -- @DFunLike.coe A Nat (fun x => Nat) funlikeA (@f n) m
#check f m          -- @DFunLike.coe A Nat (fun x => Nat) funlikeA (@f ?m.1) m

[Aaron Liu]

Well it's all the same app syntax

[Aaron Liu]

all processed at once

[Robin Arnez]

Yeah, similarly

#check id (b := 5) (fun a b => a + b) 7

works even though it might be unexpected