Function i8_fmt 

pub open spec fn i8_fmt() -> I8Fmt

{
    Mapped {
        inner: Fixed::<1>,
        mapper: (|i: Seq<u8>| i[0] as i8, |o: i8| seq![o as u8]),
    }
}