dot notation and explicit implicit parameters

Stream: general

[Mathieu Guay-Paquet]

I like dot notation (writing B.some_function when (B : bla) and bla.some_function is a function which takes an explicit bla parameter), and I know how to use 'at' notation to specify implicit parameters (for example, writing @some_function 5 when some_function takes an implicit natural number argument), but I can't seem to use both at the same time:

inductive bla | B | L | A
open bla -- to shorten 'bla.B' to just 'B'
def bla.some_function (b : bla) {n : nat} : bool := tt

#check (B.some_function) -- bool, as expected
#check (@B.some_function) -- error: unknown identifier 'B.some_function'
#check (B.@some_function) -- error: command expected
#check (@bla.some_function B) -- Π {n : ℕ}, bool, but this is cumbersome

Is there a nice way of doing this?

Alternatively, is there a way to make function parameters implicit within a section, but explicit outside of the section? (Especially when those implicit parameters are declared via variables {X Y Z : bla}?)

[Yakov Pechersky]

section explicit

variables {bla : Sort*} (X Y Z : bla)

-- bla is implicit, X Y Z explicit
#where

section implicit

variables {X Y Z}

-- bla X Y Z all implicit
#where

end implicit

-- bla is implicit, X Y Z explicit again
#where

end explicit

[Yakov Pechersky]

https://leanprover.github.io/reference/other_commands.html

[Reid Barton]

Mathieu Guay-Paquet said:

Alternatively, is there a way to make function parameters implicit within a section, but explicit outside of the section? (Especially when those implicit parameters are declared via variables {X Y Z : bla}?)

This is approximately what parameters (X Y Z : bla) does, though there are some rough edges.

[Mathieu Guay-Paquet]

@Yakov Pechersky , I don't think that's what I'm looking for, but thanks for teaching me about #where, that's super useful!

@Reid Barton , I hadn't thought of parameters that way, interesting. Unfortunately I think that makes the value essentially fixed for the whole section, yes? My use case is that I have some function arguments which are usually inferrable (with different values each time) within a section containing a bunch of related lemmas about a structure type, but outside of this section it's useful to specify these function arguments explicitly (for example, to call the tactic by rw [some_equation_lemma] successfully, I don't think some_equation_lemma can contain implicit function arguments).

[Mathieu Guay-Paquet]

Or, more accurately, something like by rw [my_struct_value.some_equation_lemma X Y].

[Reid Barton]

I see, this doesn't exist then. I think Coq has some thing where you can change implicitness of arguments after the fact, but in Lean it's fixed.

[Mathieu Guay-Paquet]

Ah ok, at least I can stop looking now, thanks!