The embedding is a right fold interpreting each source constructor by its new counterpart:Induction on the finite source list proves that querying index returns its th element exactly when lies in range. The empty case is
list' :: [a] -> List a
list' = foldr cons' nil'nil'; the cons case shifts every tail index as established in part (b). This is the only part of Question 4 whose implementation uses the conventional list type. Articles by others on the same topic
There are currently no matching articles.