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
• Lean.Meta.TransparencyMode.none.hash = 19

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

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