pith. machine review for the scientific record. sign in
def definition def or abbrev

formatConstant

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  18def formatConstant (name source : String) (exact : Bool) : String :=

proof body

Definition body.

  19  let exactStr := if exact then "exact" else "approximate"
  20  s!"  • {name} ({exactStr})\n    Source: {source}"
  21
  22/-- Print the audit report header. -/