Function parse_matches_spec 

pub open spec fn parse_matches_spec<O: DeepView>(
    r: PResult<O>,
    spec_parse: Option<(int, O::V)>,
) -> bool

{
    &&& r is Ok <==> spec_parse is Some
    &&& r is Err <==> spec_parse is None
    &&& r matches Ok((n, v)) ==> spec_parse == Some((n as int, v.deep_view()))

}

Relates an executable parse result to its pure SpecParser result.