theorem
proved
phraseCategoryCount
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Linguistics.SyntaxUniversalsFromConfigDim on GitHub at line 22.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
19 | NP | VP | AP | PP | AdvP
20 deriving DecidableEq, Repr, BEq, Fintype
21
22theorem phraseCategoryCount : Fintype.card PhraseCategory = 5 := by decide
23
24/-- The five syntactic roles (subject, object, predicate, modifier, complement). -/
25inductive SyntacticRole where
26 | subject | object | predicate | modifier | complement
27 deriving DecidableEq, Repr, BEq, Fintype
28
29theorem syntacticRoleCount : Fintype.card SyntacticRole = 5 := by decide
30
31structure SyntaxUniversalsCert where
32 five_phrases : Fintype.card PhraseCategory = 5
33 five_roles : Fintype.card SyntacticRole = 5
34
35def syntaxUniversalsCert : SyntaxUniversalsCert where
36 five_phrases := phraseCategoryCount
37 five_roles := syntacticRoleCount
38
39end IndisputableMonolith.Linguistics.SyntaxUniversalsFromConfigDim