Function ber_length_fmt 

pub open spec fn ber_length_fmt() -> Mapped<Choice<Const<U8, u8>, LengthFmt<false>>, FnSpecMapper<Sum<u8, usize>, BerLength>>

{
    Mapped {
        inner: Choice(Const(U8, 0x80u8), super::LengthFmt::<false>),
        mapper: (
            |v: Sum<u8, usize>| match v {
                L(_) => super::BerLength::Indefinite,
                R(n) => super::BerLength::Definite(n),
            },
            |v: super::BerLength| match v {
                super::BerLength::Indefinite => L(0x80u8),
                super::BerLength::Definite(n) => R(n),
            },
        ),
    }
}