Feature request: Add more default types (and use them in examples and tutorials)

[marcoeilers]

Viper would benefit from having some additional built-in types.

For example, lots of Viper examples (e.g. in the tutorial) abstract list data structures on the heap to Viper's pure sequences. Sequences, however, often require additional assertions to prove simple properties. Automation would likely (I have some examples) be much better if we used a Nil-Cons-List-ADT instead. Thanks to the ADT plugin, we could of course do that (and get better automation), but due to the fact that sequences are built-in whereas lists must be self-declared, and sequences are advertised in the tutorial, most users will default to sequences. If Lists were built-in, Viper could offer convenient syntax that's standard in many other languages, like x :: xs.

On a similar note, @jcp19 recently requested a built-in pair (or more general tuple?) type with simple syntax (e.g., the obvious (e1, e2) syntax for constructing pairs).

If extending the core Viper language is not desirable, such additional default types could also be a part of a teaching-focused version of Viper (as opposed to standard Viper which also or mostly targets frontends) that has been discussed before and could be implemented as a plugin.