meta indenting

Stream: general

[Yaël Dillies]

What's the indenting convention for tactic writing? I'm a bit puzzled by those 3 spaces after do.

[Johan Commelin]

I think that's an artifact of "do ".length = 3

[Yaël Dillies]

Uh? Why so?

[Eric Wieser]

I guess arguably

do
  foo,
  bar

would be a better style than the style that motivates the 3 spaces:

do foo,
   bar

[Yaël Dillies]

Ah yeah, if you start on the same line.

[Rob Lewis]

There isn't one established convention, we're inconsistent about it

[Rob Lewis]

You'll also see

meta def blah := do
  foo,
  bar

[Rob Lewis]

And possibly

meta def blah := do
foo,
bar

?

[Yaël Dillies]

Yes I did :sad:

[Mario Carneiro]

I also use

do foo,
  bar,
  baz

because "visual indent" is a pain on vscode

[Mario Carneiro]

but I think you should generally prefer Rob's first version when possible, especially since that's the style in lean 4