def
definition
hardProblemCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Philosophy.HardProblemOfConsciousnessFromRS on GitHub at line 35.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
32structure HardProblemCert where
33 five_stances : Fintype.card HardProblemStance = 5
34
35def hardProblemCert : HardProblemCert where
36 five_stances := hardProblemStance_count
37
38end IndisputableMonolith.Philosophy.HardProblemOfConsciousnessFromRS