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