Conversation

Gabriella Gonzalez
@GabriellaG439
Liquid Haskell verifies that this code matches the spec: {-@ leftpad :: Char -> i : String -> n : { n : Int | len i <= n } -> { o : String | len o == n } @-} leftpad :: Char -> String -> Int -> String leftpad c i n = replicate (n - length i) c ++ i That's the full code!
Quote Tweet
Hillel
@hillelogram
·
1. Leftpad. Takes a padding character, a string, and a total length, returns the string padded with that length with that character. If length is less than string, does nothing. rise4fun.com/Dafny/nbNTl
Show this thread
5
97
Hillel
@hillelogram
Wait, does this formally prove that the first however many cvharacters are c? It doesn't look like it does, just leaves it implicit. Does it still typecheck if I do leftpad c i n = replicate (n - length i) "!" ++ i ?
1
4
Gabriella Gonzalez
@GabriellaG439
No, it does not check the contents of the prefix. I couldn't even get this minimal example to work: import Data.Set {-@ test :: x : a -> { xs : [a] | listElts xs = singleton x } @-} test :: a -> [a] test = replicate 1
2
4
Hillel
@hillelogram
I think the problem is `replicate`. This worked: {-@ type SameList a S = [a]<{\x -> x = S}> @-} {-@ test :: {n : Int | n > 0} -> x : a -> {v : SameList a x | len v = n} @-} test :: Int -> a -> [a] test 1 a = [a] test n a = a:(test (n - 1) a)
1
5