forcing inclusion of unused arguments

Stream: lean4

[Eric Wieser]

Is there a better way to force an argument to be included than a dummy let clause?

variable (m n : Nat)

def foo : Nat :=
    let _ := m
    0

#print foo

This has come up in !4#2347 (cc @Pol'tta / Kô Miyahara), where we want to include an unused typeclass argument for symmetry, but don't want to move all the arguments into the def line if we can avoid it

[Eric Wieser]

def foo : Nat := (0 : (m, _).2) works too, but seems pretty silly

[Reid Barton]

Seems not that great a solution for a def, since it affects the term

[Reid Barton]

Either one, I mean

[Eric Wieser]

Oh you're right, I missed the fact that the second one poisons the Zero instance

[Reid Barton]

I suspect there isn't a great way because the variable remover runs so late (as I understand it)

[Eric Wieser]

That's what I'm leaning towards too. Maybe we do just have to list all the variables

[Mario Carneiro]

I think the better solution is just to have an include command. The whole idea behind not including it (heh...) was as a social experiment to see how necessary it really is

[Mario Carneiro]

I don't think there are any fundamental reasons not to have such a command, it is just almost never necessary and I wouldn't really trust the existing include commands for e.g. mathport usage

[Kevin Buzzard]

Another issue with the current system is that sometimes I find myself with 20 unused variables in a tactic proof, they seem to have been put there "just in case"

[Mario Carneiro]

I think we could plausibly make them auxDecls or something to hide them from the tactic state, but that's a bit weird if you actually want them to play a role