Lean

Files: .lean
Formats as: Mathlib
Lints: Every rule that reads its code
In ur.toml: [format.lean]

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 →

Versions

Ur reads Lean as the profiles below name it. Name the versions a project targets in target; without it, Ur reads lean-4.

Profile	Dialect
`lean-4`	Lean4