partial def Duper.getForallArgumentTypes (e : Lean.Expr) : List Lean.Expr

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

def Duper.mkEmptyDatatypeExhaustivenessProof (premises : List Lean.Expr) (parents : List RuleM.ProofParent) (transferExprs : Array Lean.Expr) (c : Clause) : Lean.MetaM Lean.Expr

Equations

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

def Duper.mkDatatypeExhaustivenessProof (premises : List Lean.Expr) (parents : List RuleM.ProofParent) (transferExprs : Array Lean.Expr) (c : Clause) : Lean.MetaM Lean.Expr

Equations

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

def Duper.makeConstructorEquality (e : Lean.Expr) (ctor : Lean.ConstructorVal) (lvls : List Lean.Level) (params : Array Lean.Expr) : Lean.MetaM Lean.Expr

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.

def Duper.generateDatatypeExhaustivenessFact (idt : Lean.Expr) (paramNames : Array Lean.Name) : ProverM.ProverM Unit

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.

def Duper.generateDatatypeExhaustivenessFacts (inductiveDataTypes : List (Lean.Expr × Array Lean.Name)) : ProverM.ProverM Unit

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