TypX::StrSlice and TypX::Primitive were added separately and evolved in different ways. This pull request merges the two together so that they both work the same way and the code is more uniform. Now there is just TypX::Primitive, and StrSlice is a member of the Primitive enum:
A simplification is that the AIR type and boxing/unboxing axioms for StrSlice are now generated automatically by datatype_to_air, as was already the case for Array and Slice, rather than written manually. As a bonus, the StrSlice declarations and axioms are now emitted on demand, and are pruned away when StrSlice isn't used.
TypX::StrSlice and TypX::Primitive were added separately and evolved in different ways. This pull request merges the two together so that they both work the same way and the code is more uniform. Now there is just TypX::Primitive, and StrSlice is a member of the Primitive enum:
A simplification is that the AIR type and boxing/unboxing axioms for StrSlice are now generated automatically by datatype_to_air, as was already the case for Array and Slice, rather than written manually. As a bonus, the StrSlice declarations and axioms are now emitted on demand, and are pruned away when StrSlice isn't used.
This is an internal change that should have no effect on the user interface. This is inspired somewhat by recent revisions from https://github.com/verus-lang/verus/pull/1139 .