Documentation
Lean.Meta.TransparencyMode
Google site search
Lean.Meta.TransparencyMode
source
Imports
Init
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.
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.