pub struct WcagBypassBlocksMechanism;Expand description
A skip-to-main-content mechanism or landmark structure allows users to bypass repeated navigation blocks.
Source: WCAG 2.2 SC 2.4.1 — Bypass Blocks (Level A).
Trait Implementations§
Source§impl Prop for WcagBypassBlocksMechanism
impl Prop for WcagBypassBlocksMechanism
Source§fn kani_proof() -> TokenStream
fn kani_proof() -> TokenStream
Generate a Kani proof harness for this proposition. Read more
Source§fn verus_proof() -> TokenStream
fn verus_proof() -> TokenStream
Generate a Verus proof for this proposition. Read more
Source§fn creusot_proof() -> TokenStream
fn creusot_proof() -> TokenStream
Generate a Creusot contract proof for this proposition. Read more
Source§fn creusot_invariant_fn_name() -> &'static str
fn creusot_invariant_fn_name() -> &'static str
The name of the Creusot pearlite
#[logic] function that expresses this
proposition as a predicate over the machine state. Read moreSource§fn kani_invariant_fn_name() -> &'static str
fn kani_invariant_fn_name() -> &'static str
The name of a
#[cfg(kani)] boolean predicate function that expresses
this proposition as a Kani-evaluable invariant check. Read moreSource§fn verus_invariant_fn_name() -> &'static str
fn verus_invariant_fn_name() -> &'static str
The name of a Verus
pub open spec fn that expresses this proposition
as a Verus-verifiable predicate over the machine state. Read moreAuto Trait Implementations§
impl Freeze for WcagBypassBlocksMechanism
impl RefUnwindSafe for WcagBypassBlocksMechanism
impl Send for WcagBypassBlocksMechanism
impl Sync for WcagBypassBlocksMechanism
impl Unpin for WcagBypassBlocksMechanism
impl UnsafeUnpin for WcagBypassBlocksMechanism
impl UnwindSafe for WcagBypassBlocksMechanism
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more