Documentation

Lean.Elab.BuiltinCommand

Equations
    Instances For
      Equations
        Instances For
          Equations
            Instances For
              def Lean.Elab.Command.elabReduce.go (tk term : Syntax) (skipProofs skipTypes : Bool := true) :
              Equations
                Instances For
                  Equations
                    Instances For
                      Equations
                        Instances For

                          'Delaborate' open declarations. Current limitations:

                          • does not check whether or not successive namespaces need _root_
                          • does not combine commands with renaming clauses into a single command
                          Equations
                            Instances For