Documentation

Lake.DSL.Package

Package Declarations #

DSL definitions for packages and hooks.

source
def Lake.DSL.elabPackageCommand :
Lean.Elab.Command.CommandElab
Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Lake.DSL.PackageCommand :
      Type
      Equations
        Instances For
          source
          instance Lake.DSL.instCoePackageCommandCommand :
          Coe PackageCommand Lean.Command
          Equations
            source
            def Lake.DSL.expandPostUpdateDecl :
            Lean.Macro
            Equations
              Instances For