Trait agnes::label::TakeElemByNat

pub trait TakeElemByNat<N> {
    type Elem;
    type Rest;
    fn take_elem(self) -> (Self::Elem, Self::Rest);
}

Take an element from a cons-list using typenum natural number.

Associated Types

type Elem

Type of taken element.

type Rest

Type of remaining cons-list after element was taken.

Loading content...

Required methods

fn take_elem(self) -> (Self::Elem, Self::Rest)

Take the element from this cons-list.

Loading content...

Implementors

impl<H, T> TakeElemByNat<UTerm> for Cons<H, T>

type Elem = H

type Rest = T

fn take_elem(self) -> (H, T)

impl<H, T> TakeElemByNat<UInt<UTerm, B1>> for Cons<H, T> where
    T: TakeElemByNat<UTerm>, 

type Elem = <T as TakeElemByNat<UTerm>>::Elem

type Rest = Cons<H, <T as TakeElemByNat<UTerm>>::Rest>

fn take_elem(self) -> (Self::Elem, Self::Rest)

impl<H, T, N> TakeElemByNat<UInt<N, B0>> for Cons<H, T> where
    N: Sub<B1>,
    T: TakeElemByNat<UInt<Sub1<N>, B1>>, 

type Elem = <T as TakeElemByNat<UInt<Sub1<N>, B1>>>::Elem

type Rest = Cons<H, <T as TakeElemByNat<UInt<Sub1<N>, B1>>>::Rest>

fn take_elem(self) -> (Self::Elem, Self::Rest)

impl<H, T, N, B> TakeElemByNat<UInt<UInt<N, B>, B1>> for Cons<H, T> where
    T: TakeElemByNat<UInt<UInt<N, B>, B0>>, 

type Elem = <T as TakeElemByNat<UInt<UInt<N, B>, B0>>>::Elem

type Rest = Cons<H, <T as TakeElemByNat<UInt<UInt<N, B>, B0>>>::Rest>

fn take_elem(self) -> (Self::Elem, Self::Rest)

Loading content...