Package Declarations

DSL definitions for packages and hooks.

def Lake.DSL.elabPackageCommand : Lean.Elab.Command.CommandElab

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Lake.DSL.PackageCommand : Type

Equations

• Lake.DSL.PackageCommand = Lean.TSyntax `Lake.DSL.packageCommand

instance Lake.DSL.instCoePackageCommandCommand : Coe PackageCommand Lean.Command

Equations

• Lake.DSL.instCoePackageCommandCommand = { coe := fun (x : Lake.DSL.PackageCommand) => { raw := x.raw } }

def Lake.DSL.expandPostUpdateDecl : Lean.Macro

Equations

• One or more equations did not get rendered due to their size.