cross: list: add more convenient indexing

crates/cross/src/compound/list/mod.rs

@@ -21,6 +21,36 @@ pub trait Indexable<P: Peano> {
     fn set(&mut self, v: Self::Element);
 }
 
+pub trait IndexableExplicit {
+    fn get<P: Peano>(&self) -> <Self as Indexable<P>>::Element
+    where
+        Self: Indexable<P>,
+        Self::Element: Copy,
+    {
+        Indexable::get(self)
+    }
+    fn get_ref<P: Peano>(&self) -> &<Self as Indexable<P>>::Element
+    where
+        Self: Indexable<P>,
+    {
+        Indexable::get_ref(self)
+    }
+    fn get_mut<P: Peano>(&mut self) -> &mut <Self as Indexable<P>>::Element
+    where
+        Self: Indexable<P>,
+    {
+        Indexable::get_mut(self)
+    }
+    fn set<P: Peano>(&mut self, v: Self::Element)
+    where
+        Self: Indexable<P>,
+    {
+        Indexable::set(self, v)
+    }
+}
+
+impl<L> IndexableExplicit for L {}
+
 /// convenience to lookup the type of the element at index `P` of list `L`.
 pub type ElementAt<P, L> = <L as Indexable<P>>::Element;
 

crates/cross/src/compound/peano.rs

@@ -30,6 +30,14 @@ mod exports {
     pub type P5 = PNext<P4>;
     pub type P6 = PNext<P5>;
     pub type P7 = PNext<P6>;
+    pub type P8 = PNext<P7>;
+    pub type P9 = PNext<P8>;
+    pub type P10 = PNext<P9>;
+    pub type P11 = PNext<P10>;
+    pub type P12 = PNext<P11>;
+    pub type P13 = PNext<P12>;
+    pub type P14 = PNext<P13>;
+    pub type P15 = PNext<P14>;
 }
 pub use exports::*;