def Auto.Inhabitation.getMinimalNonImpPositions (e : Lean.Expr) : Array (Array Bool)

Given an expression, return the array of positions of minimal non-implication subexpressions e.g. for ((a → b → c) → (d → e)), we have [(0, 0), (0, 1, 0), (0, 1, 1), (1, 0), (1, 1)]

Equations

• Auto.Inhabitation.getMinimalNonImpPositions e = Auto.Inhabitation.getMinimalNonImpPositions.go #[] e

def Auto.Inhabitation.getMinimalNonImpPositions.go (pos : Array Bool) (e : Lean.Expr) : Array (Array Bool)

Equations

• One or more equations did not get rendered due to their size.
• Auto.Inhabitation.getMinimalNonImpPositions.go pos e = #[pos]

def Auto.Inhabitation.getExprNonImpPosition (pos : Array Bool) (e : Lean.Expr) : Option Lean.Expr

Equations

• Auto.Inhabitation.getExprNonImpPosition pos e = Auto.Inhabitation.getExprNonImpPosition.go pos.toList e

def Auto.Inhabitation.getExprNonImpPosition.go (pos : List Bool) (e : Lean.Expr) : Option Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Auto.Inhabitation.getExprNonImpPosition.go [] e = some e
• Auto.Inhabitation.getExprNonImpPosition.go (b :: pos_2) e = none

def Auto.Inhabitation.getInhFactsFromLCtx : Lean.MetaM (Array Lemma)

Equations

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

def Auto.Inhabitation.inhFactMatchAtomTys (inhTys : Array Lemma) (atomTys : Array Lean.Expr) : Lean.MetaM (Array UMonoFact)

Equations

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

def Auto.Inhabitation.inhFactMatchAtomTys.canonicalize (inhTy : Lean.Expr) (atomTys : Array Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Auto.Inhabitation.inhFactMatchAtomTys.canonicalize inhTy atomTys = Auto.Inhabitation.inhFactMatchAtomTys.canonicalizeAtomic inhTy atomTys

def Auto.Inhabitation.inhFactMatchAtomTys.canonicalizeAtomic (inhTy : Lean.Expr) (atomTys : Array Lean.Expr) : Lean.MetaM Lean.Expr

Equations

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