Documentation

Linglib.Core.WALS.Features.F60A

WALS Feature 60A: Genitives, Adjectives and Relative Clauses #

@cite{wals-2013}

Auto-generated from WALS v2020.4 CLDF data. Do not edit by hand — regenerate with python3 scripts/gen_wals.py 60A.

Chapter 60, 138 languages.

source
inductive Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses :
Type

WALS 60A values.

Instances For
    source
    instance Core.WALS.F60A.instDecidableEqGenitivesAdjectivesAndRelativeClauses :
    DecidableEq GenitivesAdjectivesAndRelativeClauses
    Equations
    source
    instance Core.WALS.F60A.instBEqGenitivesAdjectivesAndRelativeClauses :
    BEq GenitivesAdjectivesAndRelativeClauses
    Equations
    source
    def Core.WALS.F60A.instBEqGenitivesAdjectivesAndRelativeClauses.beq :
    GenitivesAdjectivesAndRelativeClauses → GenitivesAdjectivesAndRelativeClauses → Bool
    Equations
    Instances For
      source
      def Core.WALS.F60A.instReprGenitivesAdjectivesAndRelativeClauses.repr :
      GenitivesAdjectivesAndRelativeClauses → Nat → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        instance Core.WALS.F60A.instReprGenitivesAdjectivesAndRelativeClauses :
        Repr GenitivesAdjectivesAndRelativeClauses
        Equations
        source
        def Core.WALS.F60A.allData :
        List (Datapoint GenitivesAdjectivesAndRelativeClauses)

        Complete WALS 60A dataset (138 languages).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Core.WALS.F60A.total_count :
          allData.length = 138
          source
          theorem Core.WALS.F60A.count_weaklyDifferentiated :
          (List.filter (fun (x : Datapoint GenitivesAdjectivesAndRelativeClauses) => x.value == GenitivesAdjectivesAndRelativeClauses.weaklyDifferentiated) allData).length = 15
          source
          theorem Core.WALS.F60A.count_genitivesAndAdjectivesCollapsed :
          (List.filter (fun (x : Datapoint GenitivesAdjectivesAndRelativeClauses) => x.value == GenitivesAdjectivesAndRelativeClauses.genitivesAndAdjectivesCollapsed) allData).length = 8
          source
          theorem Core.WALS.F60A.count_genitivesAndRelativeClausesCollapsed :
          (List.filter (fun (x : Datapoint GenitivesAdjectivesAndRelativeClauses) => x.value == GenitivesAdjectivesAndRelativeClauses.genitivesAndRelativeClausesCollapsed) allData).length = 2
          source
          theorem Core.WALS.F60A.count_adjectivesAndRelativeClausesCollapsed :
          (List.filter (fun (x : Datapoint GenitivesAdjectivesAndRelativeClauses) => x.value == GenitivesAdjectivesAndRelativeClauses.adjectivesAndRelativeClausesCollapsed) allData).length = 33
          source
          theorem Core.WALS.F60A.count_moderatelyDifferentiatedInOtherWays :
          (List.filter (fun (x : Datapoint GenitivesAdjectivesAndRelativeClauses) => x.value == GenitivesAdjectivesAndRelativeClauses.moderatelyDifferentiatedInOtherWays) allData).length = 3
          source
          theorem Core.WALS.F60A.count_highlyDifferentiated :
          (List.filter (fun (x : Datapoint GenitivesAdjectivesAndRelativeClauses) => x.value == GenitivesAdjectivesAndRelativeClauses.highlyDifferentiated) allData).length = 77
          source
          def Core.WALS.F60A.lookup (code : String) :
          Option (Datapoint GenitivesAdjectivesAndRelativeClauses)

          Look up a language by WALS code.

          Equations
          Instances For
            source
            def Core.WALS.F60A.lookupISO (iso : String) :
            Option (Datapoint GenitivesAdjectivesAndRelativeClauses)

            Look up a language by ISO 639-3 code.

            Equations
            Instances For