Documentation

Duper.Rules.DatatypeExhaustiveness

Given an expression ∀ x1 : t1, x2 : t2, ... xn : tn, b, returns [t1, t2, ..., tn]. If the given expression is not a forall expression, then getForallArgumentTypes just returns the empty list

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Creates the expression (∃ fields, e = ctor.{lvls} params fields) = True where params are the inductive datatype's parameters and fields are arguments that need to be passed into ctor for the resulting expression to have the correct inductive type

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Given an inductive datatype idt, with constructors ctor₁, ctor₂, ... ctorₙ, generates a fact of the form ∀ x : idt, x = ctor₁ ∨ x = ctor₂ ∨ ... x = ctorₙ and adds it to the passive set. For example, if idt = List Nat, then generateDatatypeExhaustivenessFact generates ∀ l : List Nat, l = [] ∨ ∃ n : Nat, ∃ l' : List Nat, l = n :: l'

        Polymorphic inductive datatypes are represented as universally quantified types paired with an array of parameters that can appear in the inductive datatype. For example, the polymorphic list datatype List α of where α : Type u is represented via idt ∀ (α : Type u), List α and paramNames #[u]

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          For each inductive datatype in inductiveDataTypes, generates an exhaustiveness lemma (e.g. ∀ l : List Nat, l = [] ∨ ∃ n : Nat, ∃ l' : List Nat, l = n :: l') and adds it to the passive set

          Equations
          Instances For