def
definition
def or abbrev
cost_ceiling_report_json
show as:
view Lean formalization →
formal statement (Lean)
98def cost_ceiling_report_json (src : String) : String :=
proof body
Definition body.
99 let cert := CostCeilingCert.fromSource src
100 mkJson cert.ok cert.errors
101