def
definition
ratToDecimal
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.URCAdapters.Audit on GitHub at line 37.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
34 mkZeros deficit s
35
36/-- Render a rational q = n / m to a fixed d-decimal string. -/
37def ratToDecimal (n : Int) (m : Nat) (d : Nat) : String :=
38 let sign := if n < 0 then "-" else ""
39 let nAbs : Nat := Int.natAbs n
40 if m = 0 then sign ++ "NaN" else
41 let scale := pow10 d
42 let scaled : Nat := (nAbs * scale) / m
43 let ip : Nat := scaled / scale
44 let fp : Nat := scaled % scale
45 let fpStr := padLeftZeros (toString fp) d
46 sign ++ toString ip ++ (if d = 0 then "" else "." ++ fpStr)
47
48end NumFmt
49
50private def boolToJson (b : Bool) : String := if b then "true" else "false"
51
52private def escape (s : String) : String :=
53 -- Minimal escaping for JSON content used here
54 s.replace "\"" "\\\""
55
56private def quote (s : String) : String := "\"" ++ escape s ++ "\""
57
58private def AuditItem.toJson (i : AuditItem) : String :=
59 let fields := [
60 "\"name\":" ++ quote i.name
61 , "\"category\":" ++ quote i.category
62 , "\"status\":" ++ quote i.status
63 , "\"usesExternalInput\":" ++ boolToJson i.usesExternalInput
64 ]
65 let fields := match i.value with
66 | some v => fields ++ ["\"value\":" ++ quote v]
67 | none => fields