Documentation

Aesop.Check

source
opaque Aesop.Check.all :
Lean.Option Bool
source
structure Aesop.Check :
Type
Instances For
    source
    def Aesop.Check.get (opts : Lean.Options) (opt : Check) :
    Bool
    Equations
      Instances For
        source
        def Aesop.Check.isEnabled {m : Type → Type} [Monad m] [Lean.MonadOptions m] (opt : Check) :
        m Bool
        Equations
          Instances For
            source
            def Aesop.Check.name (opt : Check) :
            Lean.Name
            Equations
              Instances For
                source
                def Aesop.Check.proofReconstruction :
                Check
                Equations
                  Instances For
                    source
                    def Aesop.Check.tree :
                    Check
                    Equations
                      Instances For
                        source
                        def Aesop.Check.rules :
                        Check
                        Equations
                          Instances For
                            source
                            def Aesop.Check.script :
                            Check
                            Equations
                              Instances For
                                source
                                def Aesop.Check.script.steps :
                                Check
                                Equations
                                  Instances For