Documentation

Lake.Build.Key

inductive Lake.BuildKey :

The type of keys in the Lake build store.

Instances For

    Like the default toString, but without disambiguation markers.

    Equations
    Instances For
      Equations
      Equations
      Instances For
        theorem Lake.BuildKey.eq_of_quickCmp {k : Lake.BuildKey} {k' : Lake.BuildKey} :
        k.quickCmp k' = Ordering.eqk = k'