Expand description
Primitive operations
Functions§
- lean_
bool_ to_ int8 - lean_
bool_ to_ int16 - lean_
bool_ to_ int32 - lean_
bool_ to_ int64 - lean_
bool_ to_ isize - lean_
bool_ to_ uint8 - lean_
bool_ to_ uint16 - lean_
bool_ to_ uint32 - lean_
bool_ to_ uint64 - lean_
bool_ to_ usize - lean_
box_ ⚠float - lean_
box_ ⚠float32 - lean_
box_ ⚠uint32 - lean_
box_ ⚠uint64 - lean_
box_ ⚠usize - lean_
float32_ add - lean_
float32_ beq - lean_
float32_ decLe - lean_
float32_ decLt - lean_
float32_ div - lean_
float32_ ⚠frexp - lean_
float32_ ⚠isfinite - lean_
float32_ ⚠isinf - lean_
float32_ ⚠isnan - lean_
float32_ mul - lean_
float32_ negate - lean_
float32_ ⚠of_ bits - lean_
float32_ ⚠scaleb - lean_
float32_ sub - lean_
float32_ ⚠to_ bits - lean_
float32_ to_ float - lean_
float32_ to_ int8 - lean_
float32_ to_ int16 - lean_
float32_ to_ int32 - lean_
float32_ to_ int64 - lean_
float32_ to_ isize - lean_
float32_ ⚠to_ string - lean_
float32_ to_ uint8 - lean_
float32_ to_ uint16 - lean_
float32_ to_ uint32 - lean_
float32_ to_ uint64 - lean_
float32_ to_ usize - lean_
float_ add - lean_
float_ beq - lean_
float_ decLe - lean_
float_ decLt - lean_
float_ div - lean_
float_ ⚠frexp - lean_
float_ ⚠isfinite - lean_
float_ ⚠isinf - lean_
float_ ⚠isnan - lean_
float_ mul - lean_
float_ negate - lean_
float_ ⚠of_ bits - lean_
float_ ⚠scaleb - lean_
float_ sub - lean_
float_ ⚠to_ bits - lean_
float_ to_ float32 - lean_
float_ to_ int8 - lean_
float_ to_ int16 - lean_
float_ to_ int32 - lean_
float_ to_ int64 - lean_
float_ to_ isize - lean_
float_ ⚠to_ string - lean_
float_ to_ uint8 - lean_
float_ to_ uint16 - lean_
float_ to_ uint32 - lean_
float_ to_ uint64 - lean_
float_ to_ usize - lean_
int8_ abs - lean_
int8_ add - lean_
int8_ complement - lean_
int8_ dec_ eq - lean_
int8_ dec_ le - lean_
int8_ dec_ lt - lean_
int8_ div - lean_
int8_ land - lean_
int8_ lor - lean_
int8_ mod - lean_
int8_ mul - lean_
int8_ neg - lean_
int8_ ⚠of_ big_ int - lean_
int8_ ⚠of_ int - lean_
int8_ ⚠of_ nat - lean_
int8_ shift_ left - lean_
int8_ shift_ right - lean_
int8_ sub - lean_
int8_ to_ float - lean_
int8_ to_ float32 - lean_
int8_ ⚠to_ int - lean_
int8_ to_ int16 - lean_
int8_ to_ int32 - lean_
int8_ to_ int64 - lean_
int8_ to_ isize - lean_
int8_ xor - lean_
int16_ abs - lean_
int16_ add - lean_
int16_ complement - lean_
int16_ dec_ eq - lean_
int16_ dec_ le - lean_
int16_ dec_ lt - lean_
int16_ div - lean_
int16_ land - lean_
int16_ lor - lean_
int16_ mod - lean_
int16_ mul - lean_
int16_ neg - lean_
int16_ ⚠of_ big_ int - lean_
int16_ ⚠of_ int - lean_
int16_ ⚠of_ nat - lean_
int16_ shift_ left - lean_
int16_ shift_ right - lean_
int16_ sub - lean_
int16_ to_ float - lean_
int16_ to_ float32 - lean_
int16_ ⚠to_ int - lean_
int16_ to_ int8 - lean_
int16_ to_ int32 - lean_
int16_ to_ int64 - lean_
int16_ to_ isize - lean_
int16_ xor - lean_
int32_ abs - lean_
int32_ add - lean_
int32_ complement - lean_
int32_ dec_ eq - lean_
int32_ dec_ le - lean_
int32_ dec_ lt - lean_
int32_ div - lean_
int32_ land - lean_
int32_ lor - lean_
int32_ mod - lean_
int32_ mul - lean_
int32_ neg - lean_
int32_ ⚠of_ big_ int - lean_
int32_ ⚠of_ int - lean_
int32_ ⚠of_ nat - lean_
int32_ shift_ left - lean_
int32_ shift_ right - lean_
int32_ sub - lean_
int32_ to_ float - lean_
int32_ to_ float32 - lean_
int32_ ⚠to_ int - lean_
int32_ to_ int8 - lean_
int32_ to_ int16 - lean_
int32_ to_ int64 - lean_
int32_ to_ isize - lean_
int32_ xor - lean_
int64_ abs - lean_
int64_ add - lean_
int64_ complement - lean_
int64_ dec_ eq - lean_
int64_ dec_ le - lean_
int64_ dec_ lt - lean_
int64_ div - lean_
int64_ land - lean_
int64_ lor - lean_
int64_ mod - lean_
int64_ mul - lean_
int64_ neg - lean_
int64_ ⚠of_ big_ int - lean_
int64_ ⚠of_ int - lean_
int64_ ⚠of_ nat - lean_
int64_ shift_ left - lean_
int64_ shift_ right - lean_
int64_ sub - lean_
int64_ to_ float - lean_
int64_ to_ float32 - lean_
int64_ to_ int8 - lean_
int64_ to_ int16 - lean_
int64_ to_ int32 - lean_
int64_ ⚠to_ int_ sint - lean_
int64_ to_ isize - lean_
int64_ xor - lean_
isize_ abs - lean_
isize_ add - lean_
isize_ complement - lean_
isize_ dec_ eq - lean_
isize_ dec_ le - lean_
isize_ dec_ lt - lean_
isize_ div - lean_
isize_ land - lean_
isize_ lor - lean_
isize_ mod - lean_
isize_ mul - lean_
isize_ neg - lean_
isize_ ⚠of_ big_ int - lean_
isize_ ⚠of_ int - lean_
isize_ ⚠of_ nat - lean_
isize_ shift_ left - lean_
isize_ shift_ right - lean_
isize_ sub - lean_
isize_ to_ float - lean_
isize_ to_ float32 - lean_
isize_ ⚠to_ int - lean_
isize_ to_ int8 - lean_
isize_ to_ int16 - lean_
isize_ to_ int32 - lean_
isize_ to_ int64 - lean_
isize_ xor - lean_
name_ ⚠eq - lean_
name_ ⚠hash - lean_
name_ ⚠hash_ exported - lean_
name_ ⚠hash_ exported_ b - lean_
name_ ⚠hash_ ptr - lean_
ptr_ addr - pointer address unsafe primitive
- lean_
st_ ⚠mk_ ref - lean_
st_ ⚠mk_ ref_ get - lean_
st_ ⚠mk_ ref_ reset - lean_
st_ ⚠mk_ ref_ set - lean_
st_ ⚠mk_ ref_ swap - lean_
uint8_ add - lean_
uint8_ complement - lean_
uint8_ dec_ eq - lean_
uint8_ dec_ le - lean_
uint8_ dec_ lt - lean_
uint8_ div - lean_
uint8_ land - lean_
uint8_ lor - lean_
uint8_ mod - lean_
uint8_ mul - lean_
uint8_ neg - lean_
uint8_ ⚠of_ big_ nat - lean_
uint8_ ⚠of_ nat - lean_
uint8_ ⚠of_ nat_ mk - lean_
uint8_ shift_ left - lean_
uint8_ shift_ right - lean_
uint8_ sub - lean_
uint8_ to_ float - lean_
uint8_ to_ float32 - lean_
uint8_ ⚠to_ nat - lean_
uint8_ to_ uint16 - lean_
uint8_ to_ uint32 - lean_
uint8_ to_ uint64 - lean_
uint8_ to_ usize - lean_
uint8_ xor - lean_
uint16_ add - lean_
uint16_ complement - lean_
uint16_ dec_ eq - lean_
uint16_ dec_ le - lean_
uint16_ dec_ lt - lean_
uint16_ div - lean_
uint16_ land - lean_
uint16_ lor - lean_
uint16_ mod - lean_
uint16_ mul - lean_
uint16_ neg - lean_
uint16_ ⚠of_ big_ nat - lean_
uint16_ ⚠of_ nat - lean_
uint16_ ⚠of_ nat_ mk - lean_
uint16_ shift_ left - lean_
uint16_ shift_ right - lean_
uint16_ sub - lean_
uint16_ to_ float - lean_
uint16_ to_ float32 - lean_
uint16_ ⚠to_ nat - lean_
uint16_ to_ uint8 - lean_
uint16_ to_ uint32 - lean_
uint16_ to_ uint64 - lean_
uint16_ to_ usize - lean_
uint16_ xor - lean_
uint32_ add - lean_
uint32_ complement - lean_
uint32_ dec_ eq - lean_
uint32_ dec_ le - lean_
uint32_ dec_ lt - lean_
uint32_ div - lean_
uint32_ land - lean_
uint32_ lor - lean_
uint32_ mod - lean_
uint32_ mul - lean_
uint32_ neg - lean_
uint32_ ⚠of_ big_ nat - lean_
uint32_ ⚠of_ nat - lean_
uint32_ ⚠of_ nat_ mk - lean_
uint32_ shift_ left - lean_
uint32_ shift_ right - lean_
uint32_ sub - lean_
uint32_ to_ float - lean_
uint32_ to_ float32 - lean_
uint32_ ⚠to_ nat - lean_
uint32_ to_ uint8 - lean_
uint32_ to_ uint16 - lean_
uint32_ to_ uint64 - lean_
uint32_ to_ usize - lean_
uint32_ xor - lean_
uint64_ add - lean_
uint64_ complement - lean_
uint64_ dec_ eq - lean_
uint64_ dec_ le - lean_
uint64_ dec_ lt - lean_
uint64_ div - lean_
uint64_ land - lean_
uint64_ lor - lean_
uint64_ ⚠mix_ hash - lean_
uint64_ mod - lean_
uint64_ mul - lean_
uint64_ neg - lean_
uint64_ ⚠of_ big_ nat - lean_
uint64_ ⚠of_ nat - lean_
uint64_ ⚠of_ nat_ mk - lean_
uint64_ shift_ left - lean_
uint64_ shift_ right - lean_
uint64_ sub - lean_
uint64_ to_ float - lean_
uint64_ to_ float32 - lean_
uint64_ to_ uint8 - lean_
uint64_ to_ uint16 - lean_
uint64_ to_ uint32 - lean_
uint64_ to_ usize - lean_
uint64_ xor - lean_
unbox_ ⚠float - lean_
unbox_ ⚠float32 - lean_
unbox_ ⚠uint32 - lean_
unbox_ ⚠uint64 - lean_
unbox_ ⚠usize - lean_
usize_ add - lean_
usize_ complement - lean_
usize_ dec_ eq - lean_
usize_ dec_ le - lean_
usize_ dec_ lt - lean_
usize_ div - lean_
usize_ land - lean_
usize_ lor - lean_
usize_ ⚠mix_ hash - lean_
usize_ mod - lean_
usize_ mul - lean_
usize_ neg - lean_
usize_ ⚠of_ big_ nat - lean_
usize_ ⚠of_ nat - lean_
usize_ ⚠of_ nat_ mk - lean_
usize_ shift_ left - lean_
usize_ shift_ right - lean_
usize_ sub - lean_
usize_ to_ float - lean_
usize_ to_ float32 - lean_
usize_ to_ uint8 - lean_
usize_ to_ uint16 - lean_
usize_ to_ uint32 - lean_
usize_ to_ uint64 - lean_
usize_ xor