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
- Duper.generateDatatypeExhaustivenessFacts inductiveDataTypes = inductiveDataTypes.forM fun (x : Lean.Expr × Array Lean.Name) => Duper.generateDatatypeExhaustivenessFact x.fst x.snd