Documentation

Lake.Build.Key

inductive Lake.BuildKey :

The type of keys in the Lake build store.

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

      Like the default toString, but without disambiguation markers.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem Lake.BuildKey.eq_of_quickCmp {k : Lake.BuildKey} {k' : Lake.BuildKey} :
          k.quickCmp k' = Ordering.eqk = k'