Mathlib

The style of Mathlib, Lean's library of mathematics.

Formats: Lean
In ur.toml: [format.lean] style = "mathlib"
Its options: https://leanprover-community.github.io/contribute/style.html

Formatted

Cart.lean, as written

-- What a cart costs.
def subtotal (items : List (Nat × Nat)) : Nat := items.foldl (fun sum (price, quantity) => sum + price * quantity) 0
theorem add_zero' (n:Nat) : n+0 = n := by
  simp

ur format --style mathlib Cart.lean

-- What a cart costs.
def subtotal (items : List (Nat × Nat)) : Nat :=
  items.foldl (fun sum (price, quantity) => sum + price * quantity) 0
theorem add_zero' (n : Nat) : n + 0 = n := by
  simp

Try it in the playground →

Defaults

The shared options, as Mathlib sets them when nothing configures it. Its own names for them are read from its configuration files, but ur.toml sets them by the shared name only.

Option	Default	Mathlib calls it
`width`	`100`
`indent.width`	`2`
`indent.style`
`line-ending`	`"lf"`
`trailing-comma.add`	`"preserve"`
`trailing-comma.forces-break`	`false`
`quotes`	`"preserve"`
`target`

Its own options

Mathlib takes no options of its own beyond the shared ones.