Conversation

joomy
@vowelharmony
*mind blown gif* I never thought of indexed data types as a function that case splits the indexing arg and returns a different data type in each case! Then to use a value of an indexed data type, you would have to case on the indexing arg first! (Nat if you want to split a Vec)
Image
4
23
joomy
@vowelharmony
For append: after the type signature I had `append a m n xs ys = ?12`, then I pressed c for case and said I wanted to split on m. Then I had what you see above. Then I pressed c again and said I wanted split on xs. So on and so forth. Did that help? What error are you getting?
1
1
Brendan Zabarauskas
@brendanzab
Yeah, I’ll try again later - just wasn’t clear to me. Doing the case thing was bringing up the case expression, rather than splitting the function into multiple clauses. Might have been splitting on the wrong thing
1