inductive
definition
PhonologicalFeature
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Linguistics.PhonologicalFeaturesFromConfigDim on GitHub at line 18.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
15
16namespace IndisputableMonolith.Linguistics.PhonologicalFeaturesFromConfigDim
17
18inductive PhonologicalFeature where
19 | place
20 | manner
21 | voicing
22 | nasality
23 | roundness
24 deriving DecidableEq, Repr, BEq, Fintype
25
26theorem phonologicalFeature_count : Fintype.card PhonologicalFeature = 5 := by decide
27
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