Module functions 

Auto-generated module

🤖 Generated with SplitRS

Traits

Decidable

A type whose truth value is decidable.

DecidablePred

A decidable predicate P : A → Prop.

DecidableRel

A decidable binary relation R : A → A → Prop.

Functions

build_decidable_env

Build the standard Decidable environment declarations.

dcs_ext_bounded_quantifiers

dcs_ext_constructive_markov

dcs_ext_decidable_eq_basic

dcs_ext_decidable_eq_compound

dcs_ext_decidable_typeclass

dcs_ext_dpll_procedure

dcs_ext_lem_boolean_reflection

dcs_ext_linear_ordering

dcs_ext_logical_connective_closure

dcs_ext_presburger_arithmetic

dcs_ext_semi_decidability

dcs_ext_undecidability_halting

decide_all

Decide a conjunction of a list of unit decisions.

decide_any

Decide a disjunction of a list of unit decisions.

decide_divisible

Decide whether n is divisible by d.

decide_ends_with

Decide whether a string slice ends with a suffix.

decide_eq

Decide whether a and b are equal for any PartialEq type.

decide_even

Decide whether an integer is even.

decide_finite_set_mem

Decide membership in a FiniteSet<T>.

decide_interval_non_empty

Decide whether an interval [lo, hi] is non-empty.

decide_intervals_overlap

Decide whether two intervals overlap.

decide_is_none

Decide whether an Option<T> is None.

decide_is_some

Decide whether an Option<T> is Some.

decide_le

Decide a ≤ b for any PartialOrd type.

decide_len

Decide whether a slice has the given length.

decide_lt

Decide a < b for any PartialOrd type.

decide_mem

Decide membership of x in a slice xs.

decide_nat_eq

Decide equality of two u32 values.

decide_nat_le

Decide a ≤ b for u32 values.

decide_nat_lt

Decide a < b for u32 values.

decide_non_empty

Decide whether a slice is non-empty.

decide_odd

Decide whether an integer is odd.

decide_option_eq

Decide equality for Option<T>.

decide_range

Decide whether a u32 lies in the range [lo, hi).

decide_slice_eq

Decide equality for slices of PartialEq elements.

decide_starts_with

Decide whether a string slice starts with a prefix.

decide_str_eq

Decide equality of two string slices.

decide_subset

Decide whether a FiniteSet is a subset of another.

decision_and

Decide P ∧ Q.

decision_from_result

Lift a Result<(), E> into a Decision<()>.

decision_implies

Decide P → Q given a decision of P and a function producing a decision of Q.

decision_not

Decide ¬P.

decision_or

Decide P ∨ Q (left-biased).

decision_to_result

Convert a Decision<()> into a Result<(), String>.

run_decisions

Run a series of named decisions and report the results.