recognition / URCAdapters / URCAdapters.Audit / main

def

`main`

definition

show as: view math explainer →

module: IndisputableMonolith.URCAdapters.Audit
domain: URCAdapters
line: 129 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.URCAdapters.Audit on GitHub at line 129.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

depends on

used by

formal source

 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.