Documentation

Aesop.Tree.Check

source
def Aesop.MVarClusterRef.checkIds (root : MVarClusterRef) :
Lean.CoreM Unit
Equations
    Instances For
      source
      def Aesop.MVarClusterRef.checkAcyclic (root : MVarClusterRef) :
      Lean.CoreM Unit
      Equations
        Instances For
          source
          def Aesop.MVarClusterRef.checkAcyclic.go {α : Type} (visited : IO.Ref (Array (IO.Ref α))) (current : IO.Ref α) :
          Lean.CoreM Bool
          Equations
            Instances For
              source
              def Aesop.MVarClusterRef.checkConsistentParentChildLinks.err :
              ReaderT Lean.Core.Context (StateRefT' IO.RealWorld Lean.Core.State (EIO Lean.Exception)) PUnit
              Equations
                Instances For
                  source
                  def Aesop.MVarClusterRef.checkState (root : MVarClusterRef) :
                  Lean.CoreM Unit
                  Equations
                    Instances For
                      source
                      @[inline]
                      def Aesop.MVarClusterRef.checkState.go {σ : Type} [BEq σ] [ToString σ] (id : String) (expected actual : σ) :
                      Lean.CoreM Unit
                      Equations
                        Instances For
                          source
                          def Aesop.MVarClusterRef.checkIrrelevance (root : MVarClusterRef) :
                          Lean.CoreM Unit
                          Equations
                            Instances For
                              source
                              @[inline]
                              def Aesop.MVarClusterRef.checkIrrelevance.go (id : String) (expected actual : Bool) :
                              Lean.CoreM Bool
                              Equations
                                Instances For
                                  source
                                  def Aesop.MVarClusterRef.checkMVars (root : MVarClusterRef) (rootMetaState : Lean.Meta.SavedState) :
                                  Lean.MetaM Unit
                                  Equations
                                    Instances For
                                      source
                                      def Aesop.MVarClusterRef.checkMVars.getParentInfo (r : Rapp) :
                                      Lean.CoreM (Lean.MVarId × Lean.Meta.SavedState)
                                      Equations
                                        Instances For
                                          source
                                          def Aesop.MVarClusterRef.checkMVars.checkAssignedMVars (r : Rapp) :
                                          Lean.MetaM Unit
                                          Equations
                                            Instances For
                                              source
                                              def Aesop.MVarClusterRef.checkMVars.checkDroppedMVars (r : Rapp) :
                                              Lean.MetaM Unit
                                              Equations
                                                Instances For
                                                  source
                                                  def Aesop.MVarClusterRef.checkMVars.checkGoalMVars (rootMetaState : Lean.Meta.SavedState) (g : Goal) :
                                                  Lean.MetaM Unit
                                                  Equations
                                                    Instances For
                                                      source
                                                      def Aesop.MVarClusterRef.checkMVars.checkNormMVars (rootMetaState : Lean.Meta.SavedState) (g : Goal) :
                                                      Lean.MetaM Unit
                                                      Equations
                                                        Instances For
                                                          source
                                                          def Aesop.MVarClusterRef.checkIntroducedMVars (root : MVarClusterRef) (rootMetaState : Lean.Meta.SavedState) :
                                                          Lean.MetaM Unit
                                                          Equations
                                                            Instances For
                                                              source
                                                              def Aesop.MVarClusterRef.checkInvariants (root : MVarClusterRef) (rootMetaState : Lean.Meta.SavedState) :
                                                              Lean.MetaM Unit
                                                              Equations
                                                                Instances For
                                                                  source
                                                                  def Aesop.MVarClusterRef.checkInvariantsIfEnabled (root : MVarClusterRef) (rootMetaState : Lean.Meta.SavedState) :
                                                                  Lean.MetaM Unit
                                                                  Equations
                                                                    Instances For
                                                                      source
                                                                      def Aesop.checkInvariantsIfEnabled :
                                                                      TreeM Unit
                                                                      Equations
                                                                        Instances For