def Lean.Meta.TransparencyMode.hash : TransparencyMode → UInt64

Equations

• Lean.Meta.TransparencyMode.all.hash = 7
• Lean.Meta.TransparencyMode.default.hash = 11
• Lean.Meta.TransparencyMode.reducible.hash = 13
• Lean.Meta.TransparencyMode.instances.hash = 17

instance Lean.Meta.TransparencyMode.instHashable_lean : Hashable TransparencyMode

Equations

• Lean.Meta.TransparencyMode.instHashable_lean = { hash := Lean.Meta.TransparencyMode.hash }

def Lean.Meta.TransparencyMode.lt : TransparencyMode → TransparencyMode → Bool

Equations

• Lean.Meta.TransparencyMode.reducible.lt Lean.Meta.TransparencyMode.default = true
• Lean.Meta.TransparencyMode.reducible.lt Lean.Meta.TransparencyMode.all = true
• Lean.Meta.TransparencyMode.reducible.lt Lean.Meta.TransparencyMode.instances = true
• Lean.Meta.TransparencyMode.instances.lt Lean.Meta.TransparencyMode.default = true
• Lean.Meta.TransparencyMode.instances.lt Lean.Meta.TransparencyMode.all = true
• Lean.Meta.TransparencyMode.default.lt Lean.Meta.TransparencyMode.all = true
• x✝¹.lt x✝ = false