def
definition
phonologicalFeatureCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Linguistics.PhonologicalFeaturesFromConfigDim on GitHub at line 31.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
28structure PhonologicalFeatureCert where
29 five_features : Fintype.card PhonologicalFeature = 5
30
31def phonologicalFeatureCert : PhonologicalFeatureCert where
32 five_features := phonologicalFeature_count
33
34end IndisputableMonolith.Linguistics.PhonologicalFeaturesFromConfigDim