Documentation

Lean.Meta.TransparencyMode

source
def Lean.Meta.TransparencyMode.hash :
TransparencyMode → UInt64
Instances For
    source
    @[instance_reducible]
    instance Lean.Meta.TransparencyMode.instHashable_lean :
    Hashable TransparencyMode
    source
    def Lean.Meta.TransparencyMode.toString :
    TransparencyMode → String
    Instances For
      source
      @[instance_reducible]
      instance Lean.Meta.TransparencyMode.instToString_lean :
      ToString TransparencyMode
      source
      def Lean.Meta.TransparencyMode.lt :
      TransparencyMode → TransparencyMode → Bool
      Instances For