Documentation
Lean
.
Meta
.
TransparencyMode
Search
Google site search
return to top
source
Imports
Init.Data.UInt.Basic
Imported by
Lean
.
Meta
.
TransparencyMode
.
hash
Lean
.
Meta
.
TransparencyMode
.
instHashableTransparencyMode
Lean
.
Meta
.
TransparencyMode
.
lt
source
def
Lean
.
Meta
.
TransparencyMode
.
hash
:
Lean.Meta.TransparencyMode
→
UInt64
Equations
One or more equations did not get rendered due to their size.
Instances For
source
instance
Lean
.
Meta
.
TransparencyMode
.
instHashableTransparencyMode
:
Hashable
Lean.Meta.TransparencyMode
Equations
Lean.Meta.TransparencyMode.instHashableTransparencyMode
=
{
hash
:=
Lean.Meta.TransparencyMode.hash
}
source
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.
Instances For