← Copula mathematical handbook

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

@[instance_reducible]

instance Lean.Meta.TransparencyMode.instHashable_lean : Hashable TransparencyMode

Equations

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

def Lean.Meta.TransparencyMode.toString : TransparencyMode → String

Equations

• Lean.Meta.TransparencyMode.all.toString = "all"
• Lean.Meta.TransparencyMode.default.toString = "default"
• Lean.Meta.TransparencyMode.reducible.toString = "reducible"
• Lean.Meta.TransparencyMode.instances.toString = "instances"
• Lean.Meta.TransparencyMode.implicit.toString = "implicit"
• Lean.Meta.TransparencyMode.none.toString = "none"

@[instance_reducible]

instance Lean.Meta.TransparencyMode.instToString_lean : ToString TransparencyMode

Equations

• Lean.Meta.TransparencyMode.instToString_lean = { toString := Lean.Meta.TransparencyMode.toString }

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
• x✝.lt Lean.Meta.TransparencyMode.implicit = false
• Lean.Meta.TransparencyMode.implicit.lt x✝ = true
• Lean.Meta.TransparencyMode.default.lt Lean.Meta.TransparencyMode.all = true
• x✝¹.lt x✝ = false