Why does Lean 4 Print Default Values?

Stream: lean4

[Atticus Kuhn]

I have a question about the printing in Lean 4. Here is a minimal example:

inductive a : Type
  | f (b1 : Bool := false) (b2 : Bool := false)

#reduce a.f

I expect this code to print

a.f

but it actually prints

a.f false

I would like to ask why this is? I should think that Lean doesn't need to print default variables if they have the default value. Furthermore, why does it on print one default value, but not the other? I don't understand this behavior. Is there anyone more familiar than myself with the inner workings of Lean 4 who knows why Lean 4 will print one of the default values, but not the other?

[Henrik Böving]

The reduction engine isn't really interested in things like default values, it is given an elaborated term and reduces it until it can't do any additional thing, then dumps what it came up with.

I am a little surprised that it doesn't print the second default value. Though if you

set_option pp.raw true

You will get the expected term, this hints at a bug in the delaborator that you might want to open an issue about in the Lean 4 repository.

That said #reduce is almost never the solution you are looking for, what exactly are you trying to achieve? #xy.

[Michael Stoll]

See also here.

[Atticus Kuhn]

Henrik Böving said:

That said #reduce is almost never the solution you are looking for, what exactly are you trying to achieve? #xy.

You're probably right that this is an xy-problem. What I really have is that I have a series of guard_msgs. I added a default argument, expecting it not to break the guard_msgs, but it actually did for the reason above.

[Henrik Böving]

I see, then you'll have to wait until the bug linked by Michael is fixed I'm afraid :/

[Kyle Miller]

In that thread, here is an explanation of the current situation. The pretty printer only considers omitting the last optional argument.

I want to fix it, but it's been low priority. The current behavior is an approximation rather than a bug. I think a fix would be to collect another array recording which arguments could be omitted and then to compute in the end which arguments actually can be.

This is what it should do, which I think illustrates the mild complexity of the problem:

• a.f false false -> a.f
• a.f false true -> a.f false true
• a.f true false -> a.f true
• a.f true true -> a.f true true

One could also wonder whether it should do

• a.f false true -> a.f (b2 := true)