Documentation

Aesop.Saturate

source
def Aesop.isForwardOrDestructRuleName (n : Aesop.RuleName) :
Bool
Equations
Instances For
    source
    structure Aesop.SaturateM.Context :
    Type
    Instances For
      source
      @[reducible, inline]
      abbrev Aesop.SaturateM (α : Type) :
      Type
      Equations
      Instances For
        source
        def Aesop.getSingleGoal {m : Type → Type} [Monad m] [Lean.MonadError m] (o : Aesop.RuleTacOutput) :
        m (Lean.MVarId × Lean.Meta.SavedState × Option (Array Aesop.Script.LazyStep))
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Aesop.saturateCore (rs : Aesop.LocalRuleSet) (goal : Lean.MVarId) :
          Aesop.SaturateM Lean.MVarId
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            partial def Aesop.saturateCore.go (rs : Aesop.LocalRuleSet) (goal : Lean.MVarId) :
            Aesop.SaturateM Lean.MVarId
            source
            def Aesop.saturateCore.tryNormRules (rs : Aesop.LocalRuleSet) (goal : Lean.MVarId) (mvars : Aesop.UnorderedArraySet Lean.MVarId) (preState : Lean.Meta.SavedState) :
            Aesop.SaturateM (Option Lean.MVarId)
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Aesop.saturateCore.trySafeRules (rs : Aesop.LocalRuleSet) (goal : Lean.MVarId) (mvars : Aesop.UnorderedArraySet Lean.MVarId) (preState : Lean.Meta.SavedState) :
              Aesop.SaturateM (Option Lean.MVarId)
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Aesop.saturateCore.runRule {α : Type} (goal : Lean.MVarId) (mvars : Aesop.UnorderedArraySet Lean.MVarId) (preState : Lean.Meta.SavedState) (matchResult : Aesop.IndexMatchResult (Aesop.Rule α)) :
                Aesop.SaturateM (Option (Lean.MVarId × Option (Array Aesop.Script.LazyStep)))
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Aesop.saturateCore.runFirstRule {α : Type} (goal : Lean.MVarId) (mvars : Aesop.UnorderedArraySet Lean.MVarId) (preState : Lean.Meta.SavedState) (matchResults : Array (Aesop.IndexMatchResult (Aesop.Rule α))) :
                  Aesop.SaturateM (Option Lean.MVarId)
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Aesop.saturate (rs : Aesop.LocalRuleSet) (goal : Lean.MVarId) (options : Aesop.Options') :
                    Lean.MetaM Lean.MVarId
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For