Documentation

Linglib.Core.WALS.Features.F17A

WALS Feature 17A: Rhythm Types #

@cite{wals-2013}

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

Chapter 17, 323 languages.

source
inductive Core.WALS.F17A.RhythmTypes :
Type

WALS 17A values.

Instances For
    source
    instance Core.WALS.F17A.instDecidableEqRhythmTypes :
    DecidableEq RhythmTypes
    Equations
    source
    instance Core.WALS.F17A.instBEqRhythmTypes :
    BEq RhythmTypes
    Equations
    source
    def Core.WALS.F17A.instBEqRhythmTypes.beq :
    RhythmTypes → RhythmTypes → Bool
    Equations
    Instances For
      source
      instance Core.WALS.F17A.instReprRhythmTypes :
      Repr RhythmTypes
      Equations
      source
      def Core.WALS.F17A.instReprRhythmTypes.repr :
      RhythmTypes → Nat → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Core.WALS.F17A.allData :
        List (Datapoint RhythmTypes)

        Complete WALS 17A dataset (323 languages).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Core.WALS.F17A.total_count :
          allData.length = 323
          source
          theorem Core.WALS.F17A.count_trochaic :
          (List.filter (fun (x : Datapoint RhythmTypes) => x.value == RhythmTypes.trochaic) allData).length = 153
          source
          theorem Core.WALS.F17A.count_iambic :
          (List.filter (fun (x : Datapoint RhythmTypes) => x.value == RhythmTypes.iambic) allData).length = 31
          source
          theorem Core.WALS.F17A.count_dualBothTrochaicAndIambic :
          (List.filter (fun (x : Datapoint RhythmTypes) => x.value == RhythmTypes.dualBothTrochaicAndIambic) allData).length = 4
          source
          theorem Core.WALS.F17A.count_undetermined :
          (List.filter (fun (x : Datapoint RhythmTypes) => x.value == RhythmTypes.undetermined) allData).length = 37
          source
          theorem Core.WALS.F17A.count_noRhythmicStress :
          (List.filter (fun (x : Datapoint RhythmTypes) => x.value == RhythmTypes.noRhythmicStress) allData).length = 98
          source
          def Core.WALS.F17A.lookup (code : String) :
          Option (Datapoint RhythmTypes)

          Look up a language by WALS code.

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

            Look up a language by ISO 639-3 code.

            Equations
            Instances For