Documentation

Aesop.Tree.Check

source
def Aesop.MVarClusterRef.checkIds (root : MVarClusterRef) :
Lean.CoreM Unit
Instances For
    source
    def Aesop.MVarClusterRef.checkAcyclic (root : MVarClusterRef) :
    Lean.CoreM Unit
    Instances For
      source
      def Aesop.MVarClusterRef.checkState (root : MVarClusterRef) :
      Lean.CoreM Unit
      Instances For
        source
        def Aesop.MVarClusterRef.checkIrrelevance (root : MVarClusterRef) :
        Lean.CoreM Unit
        Instances For
          source
          def Aesop.MVarClusterRef.checkMVars (root : MVarClusterRef) (rootMetaState : Lean.Meta.SavedState) :
          Lean.MetaM Unit
          Instances For
            source
            def Aesop.MVarClusterRef.checkIntroducedMVars (root : MVarClusterRef) (rootMetaState : Lean.Meta.SavedState) :
            Lean.MetaM Unit
            Instances For
              source
              def Aesop.MVarClusterRef.checkInvariants (root : MVarClusterRef) (rootMetaState : Lean.Meta.SavedState) :
              Lean.MetaM Unit
              Instances For
                source
                def Aesop.MVarClusterRef.checkInvariantsIfEnabled (root : MVarClusterRef) (rootMetaState : Lean.Meta.SavedState) :
                Lean.MetaM Unit
                Instances For
                  source
                  def Aesop.checkInvariantsIfEnabled :
                  TreeM Unit
                  Instances For