def Auto.isFamily (tyctorname : Lean.Name) : Lean.CoreM Bool

Test whether a given inductive type is explicitly and inductive family. i.e., return false iff numParams match the number of arguments of the type constructor

Equations

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

def Auto.isIndProp (tyctorname : Lean.Name) : Lean.CoreM Bool

Test whether a given inductive type is an inductively defined proposition

Equations

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

def Auto.isSimpleCtor (ctorname : Lean.Name) : Lean.CoreM Bool

Whether the constructor is monomorphic after all parameters are instantiated.

Equations

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

def Auto.isSimpleInductive (tyctorname : Lean.Name) : Lean.CoreM Bool

Returns true iff the inductive type is not explicitly an inductive family, and all constructors of this inductive type are simple (refer to isSimpleCtor)

Equations

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

structure Auto.SimpleIndVal : Type

• name : Lean.Name

  Name of type constructor

• type : Lean.Expr

  Instantiated type constructor

• ctors : Array (Lean.Expr × Lean.Expr)

  Array of (instantiated_ctor, type_of_instantiated_constructor)

• projs : Option (Array Lean.Expr)

  Instantiated projections

instance Auto.instToMessageDataSimpleIndVal : Lean.ToMessageData SimpleIndVal

Equations

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

def Auto.SimpleIndVal.zetaReduce (si : SimpleIndVal) : Lean.MetaM SimpleIndVal

Equations

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

structure Auto.CollectInduct.State : Type

For a given type constructor tyctor, CollectIndState[tyctor] is an array of (instantiated_tyctor, [SimpleIndVal associated to tyctor])

• recorded : Std.HashMap Lean.Name (Array Lean.Expr)
• sis : Array (Array SimpleIndVal)

@[reducible, inline]

abbrev Auto.IndCollectM (α : Type) : Type

Equations

• Auto.IndCollectM = StateRefT' IO.RealWorld Auto.CollectInduct.State Lean.MetaM

def Auto.setSis (field : Array (Array SimpleIndVal)) : IndCollectM PUnit

Equations

• Auto.setSis field = modify fun (st : Auto.CollectInduct.State) => { recorded := st.recorded, sis := field }

def Auto.getSis : IndCollectM (Array (Array SimpleIndVal))

Equations

• Auto.getSis = do let st ← get pure st.sis

def Auto.setRecorded (field : Std.HashMap Lean.Name (Array Lean.Expr)) : IndCollectM PUnit

Equations

• Auto.setRecorded field = modify fun (st : Auto.CollectInduct.State) => { recorded := field, sis := st.sis }

def Auto.getRecorded : IndCollectM (Std.HashMap Lean.Name (Array Lean.Expr))

Equations

• Auto.getRecorded = do let st ← get pure st.recorded

partial def Auto.collectExprSimpleInduct : Lean.Expr → IndCollectM Unit

def Auto.collectExprsSimpleInduct (es : Array Lean.Expr) : Lean.MetaM (Array (Array SimpleIndVal))

Equations

• Auto.collectExprsSimpleInduct es = do let __discr ← StateRefT'.run (Array.mapM Auto.collectExprSimpleInduct es) { } match __discr with | (fst, st) => pure st.sis