pub open spec fn productive_parser<T>(parser: ParserFnSpec<T>) -> boolExpand description
{ forall |input: Seq<u8>| #[trigger] parser(input) matches Some((n, _)) ==> n > 0 }The functional version of Productive.
pub open spec fn productive_parser<T>(parser: ParserFnSpec<T>) -> bool{ forall |input: Seq<u8>| #[trigger] parser(input) matches Some((n, _)) ==> n > 0 }The functional version of Productive.