Documentation

Lake.DSL.Config

source
opaque Lake.DSL.dummyDir :
System.FilePath

A dummy default constant for __dir__ to make it type check outside Lakefile elaboration (e.g., when editing).

source
opaque Lake.DSL.dummyGetConfig? :
Lean.Name → Option String

A dummy default constant for get_config to make it type check outside Lakefile elaboration (e.g., when editing).

source
def Lake.DSL.elabDirConst :
Lean.Elab.Term.TermElab
Equations
    Instances For
      source
      def Lake.DSL.elabGetConfig :
      Lean.Elab.Term.TermElab
      Equations
        Instances For