list end-appending

Stream: Is there code for X?

[Felix Weilacher]

We think of list.cons as appending an element to the head of a list. Is there a function which appends an element to the tail? I suppose this could be accomplished by combining list.cons with two list.reverse's, but does this already exist?

If this does exist, is there a corresponding induction theorem?

[Yaël Dillies]

docs#list.concat, docs#list.reverse_induction

[Felix Weilacher]

thanks! although I am getting a 404 error with the reverse_induction link

[Junyan Xu]

docs#list.reverse_rec_on