pub trait NoLookAhead: SafeParser {
// Required method
proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>);
// Provided methods
open spec fn no_lookahead_inv(&self) -> bool { ... }
fn corollary_non_extensible(&self, i1: Seq<u8>, i2: Seq<u8>) { ... }
}Expand description
No-lookahead property for parsers.
Intuitively: the parser’s behavior does not depend on “future” bytes beyond the consumed prefix (i.e., it does not need to “look ahead”/“peek” at them to decide how to parse the prefix).
Formally: if two buffers share a common prefix that successfully parses, then they parse to the same value.
Required Methods§
Provided Methods§
Sourceopen spec fn no_lookahead_inv(&self) -> bool
open spec fn no_lookahead_inv(&self) -> bool
{ true }Dyn Compatibility§
This trait is dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety".