def Lake.lpadAscii (s : String) (c : Char) (len : Nat) : String

Equations

• Lake.lpadAscii s c len = "".pushn c (len - s.lengthAssumingAscii) ++ s

def Lake.rpadAscii (s : String) (c : Char) (len : Nat) : String

Equations

• Lake.rpadAscii s c len = s.pushn c (len - s.lengthAssumingAscii)

def Lake.zpad (n len : Nat) : String

Equations

• Lake.zpad n len = Lake.lpadAscii (toString n) '0' len

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.

def Lake.lowerHexUInt64 (n : UInt64) : String

Equations

• One or more equations did not get rendered due to their size.