search

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps
MIT License
41 stars 24 forks source link

LittleEndian.combine should not inline tuple.to_list #34

Closed andres-erbsen closed 2 years ago

andres-erbsen commented 3 years ago

LittleEndian.combine should not inline tuple.to_list. It could just take a list as input and have a simpler type.

samuelgruetter commented 3 years ago

Agreed, but on the other hand, the current type allows for concise statements split_combine and combine_split. How about defining a Fixpoint combine_list, and redefining combine in terms of tuple.to_list and combine_list? I think combine is not unfolded too often, so it shouldn't break too many proofs.

andres-erbsen commented 3 years ago

Yeah, I like your idea for backwards compat. Perhaps also have _list and _tuple of everything, and maybe even deprecate the unsuffixed version.

andres-erbsen commented 2 years ago

https://github.com/mit-plv/coqutil/issues/44 https://github.com/mit-plv/coqutil/commit/f9d2d66adbe334ac645688dab42dd76a310baaed