LeftPad icon indicating copy to clipboard operation
LeftPad copied to clipboard

Tidying up the main function

Open githwxi opened this issue 6 years ago • 0 comments

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"

githwxi avatar Dec 07 '17 17:12 githwxi