Function i16_le_fmt 

pub open spec fn i16_le_fmt() -> I16LeFmt

{
    Mapped {
        inner: Fixed::<2>,
        mapper: (
            |i: Seq<u8>| i16_le_from_bytes(array_from_seq(i)),
            |o: i16| i16_le_to_bytes(o)@,
        ),
    }
}