Documentation
Lake
.
Util
.
String
Search
return to top
source
Imports
Init.Data.Nat.Fold
Init.Data.String.Extra
Init.Data.ToString.Basic
Imported by
Lake
.
lpad
Lake
.
rpad
Lake
.
zpad
Lake
.
isHex
source
def
Lake
.
lpad
(
s
:
String
)
(
c
:
Char
)
(
len
:
Nat
)
:
String
Equations
Lake.lpad
s
c
len
=
""
.
pushn
c
(
len
-
s
.
length
)
++
s
Instances For
source
def
Lake
.
rpad
(
s
:
String
)
(
c
:
Char
)
(
len
:
Nat
)
:
String
Equations
Lake.rpad
s
c
len
=
s
.
pushn
c
(
len
-
s
.
length
)
Instances For
source
def
Lake
.
zpad
(
n
len
:
Nat
)
:
String
Equations
Lake.zpad
n
len
=
Lake.lpad
(
toString
n
)
'0'
len
Instances For
source
def
Lake
.
isHex
(
s
:
String
)
:
Bool
Returns whether a string is composed of only hexadecimal digits.
Equations
One or more equations did not get rendered due to their size.
Instances For