Skip to main content

Module functions

oxilean_std::range

Module functions 

Source
Expand description

Auto-generated module

πŸ€– Generated with SplitRS

Functions§

add_axiom
Shorthand to add an axiom to env.
and_prop
Build And a b.
app
Function application f a.
app2
Function application f a b.
app3
Function application f a b c.
app4
Function application f a b c d.
array_of
Array applied to a type argument.
arrow
Build a non-dependent arrow A -> B.
axiom_dempster_shafer_belief_ty
DempsterShafer.belief : DempsterShafer β†’ Interval Float.
axiom_dempster_shafer_plausibility_ty
DempsterShafer.plausibility : DempsterShafer β†’ Interval Float.
axiom_fuzzy_interval_alpha_cut_ty
FuzzyInterval.alpha_cut : FuzzyInterval β†’ Float β†’ Interval Float.
axiom_fuzzy_interval_ty
FuzzyInterval : Type β€” fuzzy interval for soft membership.
axiom_gauss_seidel_interval_step_ty
GaussSeidel.interval_step : Nat β†’ Interval Float β†’ Interval Float.
axiom_interval_abs_ty
Interval.abs : Interval Float β†’ Interval Float.
axiom_interval_add_ty
Interval.add : Interval Float β†’ Interval Float β†’ Interval Float β€” Moore addition.
axiom_interval_contains_ty
Interval.contains : {Ξ± : Type} β†’ [Ord Ξ±] β†’ Interval Ξ± β†’ Ξ± β†’ Prop.
axiom_interval_correct_rounding_ty
IntervalArithmetic.correctRounding : Prop β€” interval operations round outward correctly.
axiom_interval_cos_ty
Interval.cos : Interval Float β†’ Interval Float.
axiom_interval_div_ty
Interval.div : Interval Float β†’ Interval Float β†’ Interval Float β€” Moore division (partial).
axiom_interval_exp_ty
Interval.exp : Interval Float β†’ Interval Float.
axiom_interval_hi_ty
Interval.hi : {Ξ± : Type} β†’ Interval Ξ± β†’ Ξ±.
axiom_interval_hull_ty
Interval.hull : Interval Float β†’ Interval Float β†’ Interval Float β€” smallest enclosing interval.
axiom_interval_intersect_ty
Interval.intersect : Interval Float β†’ Interval Float β†’ Option (Interval Float).
axiom_interval_linear_system_solve_ty
IntervalLinearSystem.solve : Nat β†’ (Interval Float) β†’ Option (Interval Float).
axiom_interval_lo_ty
Interval.lo : {Ξ± : Type} β†’ Interval Ξ± β†’ Ξ±.
axiom_interval_log_ty
Interval.log : Interval Float β†’ Option (Interval Float) β€” log on positive intervals.
axiom_interval_midpoint_ty
Interval.midpoint : Interval Float β†’ Float β€” (lo + hi) / 2.
axiom_interval_mk_ty
Interval.mk : {Ξ± : Type} β†’ Ξ± β†’ Ξ± β†’ Interval Ξ± β€” construct from lo and hi.
axiom_interval_mul_ty
Interval.mul : Interval Float β†’ Interval Float β†’ Interval Float β€” Moore multiplication.
axiom_interval_neg_ty
Interval.neg : Interval Float β†’ Interval Float.
axiom_interval_newton_converges_ty
IntervalNewton.converges : Prop β€” the interval Newton method converges quadratically.
axiom_interval_newton_step_ty
IntervalNewton.step : (Float β†’ Float) β†’ Interval Float β†’ Interval Float β†’ Interval Float.
axiom_interval_pow_ty
Interval.pow : Interval Float β†’ Nat β†’ Interval Float.
axiom_interval_presheaf_ty
IntervalPresheaf : Type 2 β€” intervals as a presheaf on the reals.
axiom_interval_scheduling_dp_correct_ty
IntervalScheduling.dpCorrect : Prop β€” DP solution correctness for WIS.
axiom_interval_scheduling_optimal_ty
IntervalScheduling.optimalSchedule : List WeightedJob β†’ List WeightedJob.
axiom_interval_sin_ty
Interval.sin : Interval Float β†’ Interval Float.
axiom_interval_sqrt_ty
Interval.sqrt : Interval Float β†’ Option (Interval Float).
axiom_interval_sub_ty
Interval.sub : Interval Float β†’ Interval Float β†’ Interval Float β€” Moore subtraction.
axiom_interval_subset_ty
Interval.subset : Interval Float β†’ Interval Float β†’ Prop.
axiom_interval_subtraction_anticlosure_ty
IntervalArithmetic.subtraction_anticlosure : Prop β€” subtraction may expand intervals.
axiom_interval_type_ty
Interval : Type β†’ Type β€” a closed interval type parameterized by a numeric type.
axiom_interval_valid_ty
Interval.valid : {Ξ± : Type} β†’ [Ord Ξ±] β†’ Interval Ξ± β†’ Prop β€” lo ≀ hi.
axiom_interval_valued_probability_ty
IntervalValuedProbability : Type β€” interval-valued probability measure.
axiom_interval_width_ty
Interval.width : Interval Float β†’ Float β€” hi - lo.
axiom_ivp_measure_ty
IntervalValuedProbability.measure : IntervalValuedProbability β†’ Interval Float.
axiom_krawczyk_enclosure_ty
Krawczyk.enclosure_theorem : Prop β€” Krawczyk’s theorem for root enclosure.
axiom_krawczyk_operator_ty
Krawczyk.operator : (Float β†’ Float) β†’ Interval Float β†’ Interval Float.
axiom_modal_interval_dual_ty
ModalInterval.dual : ModalInterval β†’ ModalInterval β€” dual of a modal interval.
axiom_modal_interval_ty
ModalInterval : Type β€” modal interval arithmetic (proper and improper intervals).
axiom_moore_fundamental_theorem_ty
MooreArithmetic.fundamental_theorem : Prop β€” fundamental theorem of interval arithmetic.
axiom_moore_inclusion_monotone_ty
MooreArithmetic.inclusion_monotone : Prop β€” inclusion monotonicity of Moore arithmetic.
axiom_range_all_iff_ty
Range.all_iff : Prop β€” Range.all r p = true ↔ βˆ€ n ∈ r, p n = true.
axiom_range_any_iff_ty
Range.any_iff : Prop β€” Range.any r p = true ↔ βˆƒ n ∈ r, p n = true.
axiom_range_foldl_correct_ty
Range.foldl_correct : Prop β€” foldl over ranges is correct with respect to List.foldl.
axiom_segment_tree_query_ty
SegmentTree.query : {Ξ± : Type} β†’ {n : Nat} β†’ SegmentTree Ξ± n β†’ Nat β†’ Nat β†’ Ξ±.
axiom_segment_tree_ty
SegmentTree : Type β†’ Nat β†’ Type β€” segment tree for interval range queries.
axiom_segment_tree_update_ty
SegmentTree.update : {Ξ± : Type} β†’ {n : Nat} β†’ SegmentTree Ξ± n β†’ Nat β†’ Ξ± β†’ SegmentTree Ξ± n.
axiom_validated_numerics_enclosure_ty
ValidatedNumerics.enclosure : (Float β†’ Float) β†’ Interval Float β†’ Prop.
axiom_weighted_job_ty
IntervalScheduling.WeightedJob : Type β€” weighted job for interval scheduling.
bool_ty
Bool type constant.
build_range_env
Build the Range type, iteration protocols, operations, and theorems.
default_pi
A default (explicit) Pi binder.
eq_expr
Build Eq @{} ty a b.
eq_true
Build BEq.beq a b = Bool.true.
ge_nat
Build Nat.ge a b (= Nat.le b a).
iff
Iff applied to two propositions.
implicit_pi
An implicit Pi binder.
inst_pi
An instance-implicit Pi binder.
le_nat
Build Nat.le a b.
list_of
List applied to a type argument.
lt_nat
Build Nat.lt a b.
mk_array_range
Build Array.range n.
mk_for_in
Build ForIn.forIn container init body.
mk_iterator_has_next
Build Iterator.hasNext state.
mk_iterator_next
Build Iterator.next state.
mk_list_enum_from
Build List.enumFrom start l.
mk_list_iota
Build List.iota n.
mk_list_range
Build List.range n.
mk_range
Build Range.mk start stop step.
mk_range_all
Build Range.all r pred.
mk_range_any
Build Range.any r pred.
mk_range_contains
Build Range.contains r n.
mk_range_foldl
Build Range.foldl f init r.
mk_range_for_m
Build Range.forM r body.
mk_range_is_empty
Build Range.isEmpty r.
mk_range_of_nat
Build Range.ofNat start stop.
mk_range_single
Build Range.single n.
mk_range_size
Build Range.size r.
mk_range_start
Build Range.start r.
mk_range_step
Build Range.step r.
mk_range_stop
Build Range.stop r.
mk_range_to_list
Build Range.toList r.
mk_range_with_step
Build Range.withStep start stop step.
mod_nat
Build Nat.mod a b.
monad_of
Monad applied to a type constructor.
nat_ty
Nat type constant.
option_of
Option applied to a type argument.
prod_of
Prod applied to two type arguments.
prop
Prop: Sort 0.
range_iterator_ty
RangeIterator type constant.
range_ty
Range type constant.
register_range_extended
Register all extended Range/Interval axioms into the environment.
rng_ext_add_axiom
rng_ext_and
rng_ext_app
rng_ext_app2
rng_ext_app3
rng_ext_arrow
rng_ext_bool
rng_ext_eq
rng_ext_float
rng_ext_iff
rng_ext_interval
rng_ext_interval_of
rng_ext_ipi
rng_ext_le
rng_ext_lt
rng_ext_nat
rng_ext_pi
rng_ext_prop
rng_ext_type1
rng_ext_type2
sub_nat
Build Nat.sub a b.
type1
Type 1: Sort 1.
type2
Type 2: Sort 2.
type_to_type
Type β†’ Type (kind of a type constructor like a monad).
unit_ty
Unit type constant.