Documentation

Lake.Config.LeanExeConfig

structure Lake.LeanExeConfig (name : Lean.Name) extends Lake.LeanConfig :

A Lean executable's declarative configuration.

Instances For
    instance Lake.LeanExeConfig.instConfigMeta :
    ConfigInfo `Lake.LeanExeConfig
    Equations
      @[reducible, inline]

      The executable's name.

      Equations
        Instances For