Function mm0b_parser::parse_cmd [−][src]
pub fn parse_cmd(
mmb: &[u8],
starts_at: usize
) -> Result<(u8, u32, usize), ParseError>
Expand description
From a (full) mmb file and a start position, parse the raw data
for a command, which is a [(u8, u32)]
pair of (cmd, data)
.
Also returns the new start position, which is the old position
plus the size of cmd
, and the size of data
which varies
despite ending up as a u32
.
For UnifyCmd
and ProofCmd
, the (u8, u32)
pair is used to make the corresponding cmd.
For DeclIter
, the u8
is a StmtCmd
, and the u32
is the length of the proof iterator
that should be constructed for that statement.