Documentation

Lake.Config.LeanExeConfig

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

A Lean executable's declarative configuration.

Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[reducible, inline]

      The executable's name.

      Equations
      Instances For