Documentation

Aesop.Util.Tactic.Ext

source
structure Aesop.ExtResult :
Type
Instances For
    source
    def Aesop.straightLineExt (goal : Lean.MVarId) :
    Lean.MetaM ExtResult
    Equations
      Instances For
        source
        partial def Aesop.straightLineExt.go (goal : Lean.MVarId) (depth : Nat) (commonFVarIds : Array Lean.FVarId) :
        Lean.MetaM ExtResult
        source
        def Aesop.straightLineExtProgress (goal : Lean.MVarId) :
        Lean.MetaM ExtResult
        Equations
          Instances For