LeftPad
LeftPad copied to clipboard
Tidying up the main function
Thanks for writing this! I tidied up the main function a bit:
implement main0(argc, argv) =
if
argc = 3
then let
val c = '0'
val s = g1ofg0(argv[1])
val pad = g1ofg0(g0string2int(argv[2]))
in
if isneqz(s) && pad > 0
then (
let
prval _ = lemma_not_empty(s) where {
extern praxi
lemma_not_empty{n:int}(x:string(n)):[n > 0] void
}
prval _ = lemma_not_zero(pad) where {
extern praxi
lemma_not_zero{n:int}(x:int(n)):[n > 0] void
}
val (pf | res) = left_pad(i2ssz(pad),c, string1_copy(s))
in
println! ("padding: ", res); strnptr_free(res);
end
) else print "Usage: left-pad <string-to-pad> <pad-length>\n"
end else print "Usage: left-pad <string-to-pad> <pad-length>\n"