def Aesop.BuiltinRules.matchSubstitutableIff? (e : Lean.Expr) : Option (Lean.Expr × Lean.Expr)

Equations

• Aesop.BuiltinRules.matchSubstitutableIff? e = match e.iff? with | some (lhs, rhs) => if (lhs.isFVar || rhs.isFVar) = true then pure (lhs, rhs) else failure | x => failure

def Aesop.BuiltinRules.prepareIff? (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) : ScriptM (Option (Lean.MVarId × Lean.FVarId))

Equations

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

def Aesop.BuiltinRules.prepareIffs (mvarId : Lean.MVarId) (fvarIds : Array Lean.FVarId) : ScriptM (Lean.MVarId × Array Lean.FVarId)

Equations

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

def Aesop.BuiltinRules.substEqs? (goal : Lean.MVarId) (fvarIds : Array Lean.FVarId) : ScriptM (Option Lean.MVarId)

Equations

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

def Aesop.BuiltinRules.substEqsAndIffs? (goal : Lean.MVarId) (fvarIds : Array Lean.FVarId) : ScriptM (Option Lean.MVarId)

Equations

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

def Aesop.BuiltinRules.subst : RuleTac

Equations

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