indentation within defs of terms of structure

Stream: mathlib4

[Anthony Bordg]

When defining a term of a structure with the where command, fields should be indented one space, but how many spaces should proofs within these fields be indented, one or two spaces?

[Kyle Miller]

I thought fields were two spaces?

[Kyle Miller]

For example, here: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Combinatorics/SimpleGraph/Basic.lean#L114-L124

Two spaces for fields, and then a total of four spaces for the continued value (like the tactic script)

[Anthony Bordg]

Kyle Miller said:

I thought fields were two spaces?

I'm not talking about structure, class or instance (of a class), but about the definition of a term belonging to a structure.

[Kyle Miller]

That instance is defining a term of a structure (it could be written @[instance] def ... where ...)

[Kyle Miller]

Can you give an example?

[Anthony Bordg]

Does it make any difference wrt indentation if fields stand on multiple lines vs a def where every field holds on a single line?

[Kyle Miller]

def foo : S where
  x := 1
  y := 2
  h := by
    tac1
    tac2
  z := 3
  f :=
    fun x =>
      let a := x + 1
      a + a

[Kyle Miller]

I think it's always that indentation is a multiple of two spaces, though there might be some exceptions if it's an expression in parentheses or other delimiters that's being continued.

[Anthony Bordg]

My question was motivated by the fact that today I wrote something of the form

def foo : S where
    x := 1
    y := 2
    hx := by tact1
    hy := by tact2

each field indented with 2 spaces and I got a linter error after a git push, it wanted the fields to be indented with only one space.

[Kyle Miller]

I'm confused — each field is indented with 4 spaces there

[Kyle Miller]

When you say "space" are you meaning "tab"? In the mathlib default VS Code settings, each tab key is replaced with two spaces:

"editor.insertSpaces": true,
"editor.tabSize": 2,

[Anthony Bordg]

I realised my confusion now! Thank you.