lean icon indicating copy to clipboard operation
lean copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

chore(*): Swap `append` and `concat`

Open YaelDillies opened this issue 3 years ago • 1 comments

What's called append is concatenation in other languages and what's called concat is appending. This renames

  • has_append.append → has_concat.concat
  • buffer.append → buffer.concat
  • list.append → list.concat
  • dlist.append → dlist.concat
  • dlist.concat → dlist.append
  • vector.append → vector.concat
  • string.append → string.concat
  • name.append → name.concat

YaelDillies avatar Sep 19 '22 18:09 YaelDillies

Pending discussion on Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/append.20and.20concat/near/299602232

gebner avatar Sep 19 '22 18:09 gebner