structure Auto.Embedding.Lam.IndInfo : Type

• type : LamSort
• ctors : List (LamSort × LamTerm)
• projs : Option (List (LamSort × LamTerm))

def Auto.Embedding.Lam.IndInfo.toString (i : IndInfo) : String

Equations

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

instance Auto.Embedding.Lam.instToStringIndInfo : ToString IndInfo

Equations

• Auto.Embedding.Lam.instToStringIndInfo = { toString := Auto.Embedding.Lam.IndInfo.toString }

def Auto.Embedding.Lam.IndInfo.mpAll?Aux (rw : LamTerm) : List (LamSort × LamTerm) → Option (List (LamSort × LamTerm))

Equations

• Auto.Embedding.Lam.IndInfo.mpAll?Aux rw [] = some []
• Auto.Embedding.Lam.IndInfo.mpAll?Aux rw ((s, t) :: tail) = match rw.mpAll? t, Auto.Embedding.Lam.IndInfo.mpAll?Aux rw tail with | some t', some tail' => some ((s, t') :: tail') | x, x_1 => none

def Auto.Embedding.Lam.IndInfo.mpAll? (rw : LamTerm) (ii : IndInfo) : Option IndInfo

Equations

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

@[reducible, inline]

abbrev Auto.Embedding.Lam.MutualIndInfo : Type

Equations

• Auto.Embedding.Lam.MutualIndInfo = List Auto.Embedding.Lam.IndInfo

def Auto.Embedding.Lam.MutualIndInfo.mpAll? (rw : LamTerm) : MutualIndInfo → Option MutualIndInfo

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.MutualIndInfo.mpAll? rw [] = some []