def
definition
runAudit
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 126.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
123 let cosmo := String.intercalate "," (cosmologyItems.map (fun i => AuditItem.toJson i))
124 "{\"items\":[" ++ body ++ "],\"cosmology\":[" ++ cosmo ++ "]}"
125
126def runAudit : IO Unit := do
127 IO.println audit_json_report
128
129def main : IO Unit := runAudit
130
131end URCAdapters
132end IndisputableMonolith
133
134def main : IO Unit := IndisputableMonolith.URCAdapters.runAudit