There is a question which I don't really quite understand. Can someone explain the answer to me?
I get the first part: the declaration of the "function" however the rest of it I am quite confused. Variables do not need to be declared for this type of exercise.
Insert a sequence at a given location in another sequence.
For example, if the sequence <z,x,z> were to be inserted at location 2 of the sequence <x,y,z>,
the result would be the sequence <x,z,x,z,y,z>.
(Note that this operation is defined only for locations that are within the sequence, in above
example, locations 1, 2 and 3).
The answer is given below.
insert: seq X → NAT → seq X ⇸ seq X n < #t ⇒ (i < n ⇒ (insert s n t) i = t i ∧ n ≤ i < n ⇒ (insert s n t) i = s(i – n + 1) ∧ i ≥ n + #s ⇒ (insert s n t) i = t(i - #s))