def
definition
methodReport_ok
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.URCAdapters.CPMReports on GitHub at line 28.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
25 let _ := URCGenerators.toyModel_cmin_pos
26 "CPM Method Report: OK"
27
28@[simp] noncomputable def methodReport_ok : String := methodReport
29
30end CPMReports
31end URCAdapters
32end IndisputableMonolith