Struct WcagTimingAdjustable 

pub struct WcagTimingAdjustable;

Each time limit can be turned off, adjusted, or extended before it expires (with real-time and 20-hour exceptions).

Source: WCAG 2.2 SC 2.2.1 — Timing Adjustable (Level A).

Trait Implementations

impl Prop for WcagTimingAdjustable

fn kani_proof() -> TokenStream

Generate a Kani proof harness for this proposition.

fn verus_proof() -> TokenStream

Generate a Verus proof for this proposition.

fn creusot_proof() -> TokenStream

Generate a Creusot contract proof for this proposition.

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.

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.

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.