pub struct WcagAudioControlAvailable;Expand description
A mechanism is available to pause, stop, or adjust audio that plays automatically for more than 3 seconds.
Source: WCAG 2.2 SC 1.4.2 — Audio Control (Level A).
Trait Implementations§
Source§impl Prop for WcagAudioControlAvailable
impl Prop for WcagAudioControlAvailable
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 WcagAudioControlAvailable
impl RefUnwindSafe for WcagAudioControlAvailable
impl Send for WcagAudioControlAvailable
impl Sync for WcagAudioControlAvailable
impl Unpin for WcagAudioControlAvailable
impl UnsafeUnpin for WcagAudioControlAvailable
impl UnwindSafe for WcagAudioControlAvailable
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