Indentation in meta code

Stream: general

[Yury G. Kudryashov]

I see both

      match names.find? m with
      | some others => return names.insert m (others.push n)
      | none => return names.insert m #[n]

and

  match name with
    | .anonymous => s
    | .num _ _ => panic s!"panic in `getModule`: did not expect numerical name: {name}."
    | .str pre s => getModule pre s

in Mathlib/Lean/Name. Which indentation style is preferred?

[Kyle Miller]

I like using the first one.