Documentation

Aesop.Search.Expansion.Simp

source
inductive Aesop.SimpResult :
Type
Instances For
    source
    def Aesop.SimpResult.newGoal? :
    Aesop.SimpResult → Option Lean.MVarId
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Aesop.mkSimpOnly (stx : Lean.Syntax) (usedSimps : Lean.Meta.Simp.UsedSimps) (includeFVars : Bool) :
      Lean.MetaM Lean.Syntax
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Aesop.mkNormSimpSyntax (normSimpUseHyps : Bool) (configStx? : Option Lean.Term) :
        Lean.MetaM Lean.Syntax.Tactic
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Aesop.mkNormSimpOnlySyntax (inGoal : Lean.MVarId) (normSimpUseHyps : Bool) (configStx? : Option Lean.Term) (usedTheorems : Lean.Meta.Simp.UsedSimps) :
          Lean.MetaM Lean.Syntax.Tactic
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Aesop.mkNormSimpContext (rs : Aesop.RuleSet) (simpConfig : Aesop.SimpConfig) :
            Lean.MetaM Lean.Meta.Simp.Context
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Aesop.simpGoal (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (simplifyTarget : optParam Bool true) (fvarIdsToSimp : optParam (Array Lean.FVarId) #[]) (usedSimps : optParam Lean.Meta.Simp.UsedSimps ∅) :
              Lean.MetaM Aesop.SimpResult
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Aesop.simpGoalWithAllHypotheses (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (simplifyTarget : optParam Bool true) (usedSimps : optParam Lean.Meta.Simp.UsedSimps ∅) :
                Lean.MetaM Aesop.SimpResult
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Aesop.simpAll (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (usedSimps : optParam Lean.Meta.Simp.UsedSimps ∅) :
                  Lean.MetaM Aesop.SimpResult
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For