def
definition
constitutionalFormsCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Governance.ConstitutionalFormsFromConfigDim on GitHub at line 31.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
28structure ConstitutionalFormsCert where
29 five_forms : Fintype.card ConstitutionalForm = 5
30
31def constitutionalFormsCert : ConstitutionalFormsCert where
32 five_forms := constitutionalForm_count
33
34end IndisputableMonolith.Governance.ConstitutionalFormsFromConfigDim