Documentation

Lean.Meta.TransparencyMode

def Lean.Meta.TransparencyMode.hash:

Lean.Meta.TransparencyMode → UInt64

Equations

One or more equations did not get rendered due to their size.

instance Lean.Meta.TransparencyMode.instHashableTransparencyMode:

Hashable Lean.Meta.TransparencyMode

Equations

Lean.Meta.TransparencyMode.instHashableTransparencyMode = { hash := Lean.Meta.TransparencyMode.hash }

def Lean.Meta.TransparencyMode.lt:

Lean.Meta.TransparencyMode → Lean.Meta.TransparencyMode → Bool

Equations

One or more equations did not get rendered due to their size.