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.