def definition def or abbrev

`mkJson`

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

formal statement (Lean)

  75private def mkJson (ok : Bool) (errors : List String) : String :=

proof body

Definition body.

  76  Lean.Json.pretty <| Lean.Json.obj [
  77    ("ok", Lean.Json.ofBool ok),
  78    ("errors", Lean.Json.arr (errors.map Lean.Json.str))
  79  ]
  80

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.

compiler_checks_report_json in IndisputableMonolith.URCAdapters.LNALReports decl_use
cost_ceiling_report_json in IndisputableMonolith.URCAdapters.LNALReports decl_use
lnal_invariants_report_json in IndisputableMonolith.URCAdapters.LNALReports decl_use
opcode_soundness_report_json in IndisputableMonolith.URCAdapters.LNALReports decl_use
schedule_neutrality_report_json in IndisputableMonolith.URCAdapters.LNALReports decl_use
su3_mask_report_json in IndisputableMonolith.URCAdapters.LNALReports decl_use
units_kgate_report_json in IndisputableMonolith.URCAdapters.LNALReports decl_use

depends on (1)

Lean names referenced from this declaration's body.

map in IndisputableMonolith.Measurement.RSNative.Core decl_use