Documentation

Aesop.BuiltinRules.Subst

source
structure Aesop.BuiltinRules.SubstitutableEq :
Type
Instances For
    source
    inductive Aesop.BuiltinRules.SubstitutableHyp :
    Type
    Instances For
      source
      def Aesop.BuiltinRules.getSubstitutableHyp (fvarId : Lean.FVarId) :
      Lean.MetaM (Option Aesop.BuiltinRules.SubstitutableHyp)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Aesop.BuiltinRules.getSubstitutableEqs (goal : Lean.MVarId) (fvarIds : Array Lean.FVarId) :
        Aesop.ScriptM (Lean.MVarId × Array Aesop.BuiltinRules.SubstitutableEq)
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Aesop.BuiltinRules.substFVars (goal : Lean.MVarId) (fvarIds : Array Lean.FVarId) :
          Aesop.ScriptM (Option Lean.MVarId)
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Aesop.BuiltinRules.subst :
            Aesop.RuleTac
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For