Documentation

Linglib.Core.WALS.Features.F143D

WALS Feature 143D: Optional Triple Negation #

@cite{wals-2013}

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

Chapter 143, 6 languages.

source
inductive Core.WALS.F143D.OptionalTripleNegation :
Type

WALS 143D values.

Instances For
    source
    instance Core.WALS.F143D.instDecidableEqOptionalTripleNegation :
    DecidableEq OptionalTripleNegation
    Equations
    source
    instance Core.WALS.F143D.instBEqOptionalTripleNegation :
    BEq OptionalTripleNegation
    Equations
    source
    def Core.WALS.F143D.instBEqOptionalTripleNegation.beq :
    OptionalTripleNegation → OptionalTripleNegation → Bool
    Equations
    Instances For
      source
      def Core.WALS.F143D.instReprOptionalTripleNegation.repr :
      OptionalTripleNegation → Nat → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        instance Core.WALS.F143D.instReprOptionalTripleNegation :
        Repr OptionalTripleNegation
        Equations
        source
        def Core.WALS.F143D.allData :
        List (Datapoint OptionalTripleNegation)

        Complete WALS 143D dataset (6 languages).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Core.WALS.F143D.total_count :
          allData.length = 6
          source
          theorem Core.WALS.F143D.count_negVNeg :
          (List.filter (fun (x : Datapoint OptionalTripleNegation) => x.value == OptionalTripleNegation.negVNeg) allData).length = 1
          source
          theorem Core.WALS.F143D.count_vNegNegOptneginfixOrPref :
          (List.filter (fun (x : Datapoint OptionalTripleNegation) => x.value == OptionalTripleNegation.vNegNegOptneginfixOrPref) allData).length = 1
          source
          theorem Core.WALS.F143D.count_negvnegNegnegvneg :
          (List.filter (fun (x : Datapoint OptionalTripleNegation) => x.value == OptionalTripleNegation.negvnegNegnegvneg) allData).length = 1
          source
          theorem Core.WALS.F143D.count_negVNegNegvnegNegtone :
          (List.filter (fun (x : Datapoint OptionalTripleNegation) => x.value == OptionalTripleNegation.negVNegNegvnegNegtone) allData).length = 1
          source
          theorem Core.WALS.F143D.count_negVNegNegVNeg :
          (List.filter (fun (x : Datapoint OptionalTripleNegation) => x.value == OptionalTripleNegation.negVNegNegVNeg) allData).length = 1
          source
          theorem Core.WALS.F143D.count_negV :
          (List.filter (fun (x : Datapoint OptionalTripleNegation) => x.value == OptionalTripleNegation.negV) allData).length = 1
          source
          def Core.WALS.F143D.lookup (code : String) :
          Option (Datapoint OptionalTripleNegation)

          Look up a language by WALS code.

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

            Look up a language by ISO 639-3 code.

            Equations
            Instances For