Documentation

Linglib.Core.WALS.Features.F144G

WALS Feature 144G: Optional Double Negation in SVO languages #

@cite{wals-2013}

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

Chapter 144, 35 languages.

source
inductive Core.WALS.F144G.OptionalDoubleNegationInSvoLanguages :
Type

WALS 144G values.

Instances For
    source
    instance Core.WALS.F144G.instDecidableEqOptionalDoubleNegationInSvoLanguages :
    DecidableEq OptionalDoubleNegationInSvoLanguages
    Equations
    source
    def Core.WALS.F144G.instBEqOptionalDoubleNegationInSvoLanguages.beq :
    OptionalDoubleNegationInSvoLanguages → OptionalDoubleNegationInSvoLanguages → Bool
    Equations
    Instances For
      source
      instance Core.WALS.F144G.instBEqOptionalDoubleNegationInSvoLanguages :
      BEq OptionalDoubleNegationInSvoLanguages
      Equations
      source
      def Core.WALS.F144G.instReprOptionalDoubleNegationInSvoLanguages.repr :
      OptionalDoubleNegationInSvoLanguages → Nat → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        instance Core.WALS.F144G.instReprOptionalDoubleNegationInSvoLanguages :
        Repr OptionalDoubleNegationInSvoLanguages
        Equations
        source
        def Core.WALS.F144G.allData :
        List (Datapoint OptionalDoubleNegationInSvoLanguages)

        Complete WALS 144G dataset (35 languages).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Core.WALS.F144G.total_count :
          allData.length = 35
          source
          theorem Core.WALS.F144G.count_snegvo :
          (List.filter (fun (x : Datapoint OptionalDoubleNegationInSvoLanguages) => x.value == OptionalDoubleNegationInSvoLanguages.snegvo) allData).length = 6
          source
          theorem Core.WALS.F144G.count_svoneg :
          (List.filter (fun (x : Datapoint OptionalDoubleNegationInSvoLanguages) => x.value == OptionalDoubleNegationInSvoLanguages.svoneg) allData).length = 8
          source
          theorem Core.WALS.F144G.count_svnego :
          (List.filter (fun (x : Datapoint OptionalDoubleNegationInSvoLanguages) => x.value == OptionalDoubleNegationInSvoLanguages.svnego) allData).length = 3
          source
          theorem Core.WALS.F144G.count_snegvo_4 :
          (List.filter (fun (x : Datapoint OptionalDoubleNegationInSvoLanguages) => x.value == OptionalDoubleNegationInSvoLanguages.snegvo_4) allData).length = 1
          source
          theorem Core.WALS.F144G.count_svoneg_5 :
          (List.filter (fun (x : Datapoint OptionalDoubleNegationInSvoLanguages) => x.value == OptionalDoubleNegationInSvoLanguages.svoneg_5) allData).length = 2
          source
          theorem Core.WALS.F144G.count_svnego_6 :
          (List.filter (fun (x : Datapoint OptionalDoubleNegationInSvoLanguages) => x.value == OptionalDoubleNegationInSvoLanguages.svnego_6) allData).length = 1
          source
          theorem Core.WALS.F144G.count_negsVO :
          (List.filter (fun (x : Datapoint OptionalDoubleNegationInSvoLanguages) => x.value == OptionalDoubleNegationInSvoLanguages.negsVO) allData).length = 1
          source
          theorem Core.WALS.F144G.count_sVNego :
          (List.filter (fun (x : Datapoint OptionalDoubleNegationInSvoLanguages) => x.value == OptionalDoubleNegationInSvoLanguages.sVNego) allData).length = 1
          source
          theorem Core.WALS.F144G.count_sNegVO :
          (List.filter (fun (x : Datapoint OptionalDoubleNegationInSvoLanguages) => x.value == OptionalDoubleNegationInSvoLanguages.sNegVO) allData).length = 2
          source
          theorem Core.WALS.F144G.count_snegvoSvnegoNegtone :
          (List.filter (fun (x : Datapoint OptionalDoubleNegationInSvoLanguages) => x.value == OptionalDoubleNegationInSvoLanguages.snegvoSvnegoNegtone) allData).length = 1
          source
          theorem Core.WALS.F144G.count_sVO :
          (List.filter (fun (x : Datapoint OptionalDoubleNegationInSvoLanguages) => x.value == OptionalDoubleNegationInSvoLanguages.sVO) allData).length = 1
          source
          theorem Core.WALS.F144G.count_sNegVO_12 :
          (List.filter (fun (x : Datapoint OptionalDoubleNegationInSvoLanguages) => x.value == OptionalDoubleNegationInSvoLanguages.sNegVO_12) allData).length = 2
          source
          theorem Core.WALS.F144G.count_svonegSvoneg :
          (List.filter (fun (x : Datapoint OptionalDoubleNegationInSvoLanguages) => x.value == OptionalDoubleNegationInSvoLanguages.svonegSvoneg) allData).length = 1
          source
          theorem Core.WALS.F144G.count_sNegVONegsvnego :
          (List.filter (fun (x : Datapoint OptionalDoubleNegationInSvoLanguages) => x.value == OptionalDoubleNegationInSvoLanguages.sNegVONegsvnego) allData).length = 1
          source
          theorem Core.WALS.F144G.count_snegVNegOSNegVNegO :
          (List.filter (fun (x : Datapoint OptionalDoubleNegationInSvoLanguages) => x.value == OptionalDoubleNegationInSvoLanguages.snegVNegOSNegVNegO) allData).length = 1
          source
          theorem Core.WALS.F144G.count_sVONegv :
          (List.filter (fun (x : Datapoint OptionalDoubleNegationInSvoLanguages) => x.value == OptionalDoubleNegationInSvoLanguages.sVONegv) allData).length = 1
          source
          theorem Core.WALS.F144G.count_svoSovVNeg :
          (List.filter (fun (x : Datapoint OptionalDoubleNegationInSvoLanguages) => x.value == OptionalDoubleNegationInSvoLanguages.svoSovVNeg) allData).length = 1
          source
          theorem Core.WALS.F144G.count_svoVsoNegvVnegNegvneg :
          (List.filter (fun (x : Datapoint OptionalDoubleNegationInSvoLanguages) => x.value == OptionalDoubleNegationInSvoLanguages.svoVsoNegvVnegNegvneg) allData).length = 1
          source
          def Core.WALS.F144G.lookup (code : String) :
          Option (Datapoint OptionalDoubleNegationInSvoLanguages)

          Look up a language by WALS code.

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

            Look up a language by ISO 639-3 code.

            Equations
            Instances For