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.