Traits
- Types used in executable code can implement View to provide a mathematical abstraction of the type. For example, Vec implements a view method that returns a Seq. For base types like bool and u8, the view V of the type is the type itself. Types only used in ghost code, such as int, nat, and Seq, do not need to implement View.