Hi! I’m having a bit of trouble understanding the difference between strong and weak specification in Coq. For instance, if I wanted to write the replicate function (given a number n and a value x, it creates a list of length n, with all elements equal to x) using the strong specification way, how would I be able to do that? Apparently I have to write an Inductive “version” of the function but how?
Definition in Haskell:
myReplicate :: Int -> a -> [a] myReplicate 0 _ =  myReplicate n x | n > 0 = x:myReplicate (n-1) x | otherwise =