Skip to main content

Module functions

oxilean_std::stream

Module functions 

Source
Expand description

Auto-generated module

πŸ€– Generated with SplitRS

Functions§

build_stream_combinators
Build extended Stream combinators in the environment.
build_stream_env
Build Stream type in the environment.
build_stream_monad
Build Stream monad operations in the environment.
build_stream_theorems
Build Stream theorems in the environment.
count_stream_decls
Count how many Stream declarations are registered in an environment.
strm_ext_automaton_ty
Stream.automaton: a stream automaton (coalgebra for Stream functor). Type: {S Ξ± : Type} β†’ (S β†’ Prod Ξ± S) β†’ S β†’ Stream Ξ±
strm_ext_bisim_coind_ty
Stream.bisim_coind: coinductive bisimulation principle. Type: {Ξ± : Type} β†’ (R : Stream Ξ± β†’ Stream Ξ± β†’ Prop) β†’ … β†’ βˆ€ s t, R s t β†’ s = t
strm_ext_bisim_ty
Stream.Bisim: the bisimulation relation between two streams. Type: {Ξ± : Type} β†’ Stream Ξ± β†’ Stream Ξ± β†’ Prop
strm_ext_bloom_filter_ty
BloomFilter.type: a streaming Bloom filter. Type: Nat β†’ Nat β†’ Type
strm_ext_bohm_tree_ty
Stream.BΓΆhmTree: BΓΆhm tree as lazy normal form of a stream term. Type: Type β†’ Type
strm_ext_circular_prog_ty
Stream.circular_prog: circular programming / tie-the-knot combinator. Type: {Ξ± Ξ² : Type} β†’ ((Stream Ξ± β†’ Ξ²) β†’ Stream Ξ± β†’ Ξ²) β†’ Stream Ξ± β†’ Ξ²
strm_ext_corec_ty
Stream.corec: corecursion principle for streams. Type: {Ξ± Οƒ : Type} β†’ (Οƒ β†’ Ξ±) β†’ (Οƒ β†’ Οƒ) β†’ Οƒ β†’ Stream Ξ±
strm_ext_corecursion_unique_ty
Stream.corecursion_unique: uniqueness of corecursive definitions. Type: {Ξ± Οƒ : Type} β†’ (f g : Οƒ β†’ Stream Ξ±) β†’ (βˆ€ s, f s = g s) β†’ Prop
strm_ext_count_min_sketch_ty
CountMinSketch.type: a streaming count-min sketch. Type: Nat β†’ Nat β†’ Type
strm_ext_diff_eq_ty
Stream.diff_eq: stream differential equation axiom. Type: {Ξ± : Type} β†’ (Stream Ξ± β†’ Stream Ξ±) β†’ Stream Ξ± β†’ Prop
strm_ext_frp_behavior_ty
FRP.Behavior: a time-varying value (FRP behavior). Type: Type β†’ Type
strm_ext_frp_event_ty
FRP.Event: a discrete stream of events with timestamps. Type: Type β†’ Type
strm_ext_frp_stepper_ty
FRP.stepper: convert a stream of events to a behavior. Type: {Ξ± : Type} β†’ Ξ± β†’ Stream Ξ± β†’ FRP.Behavior Ξ±
strm_ext_fusion_law_ty
Stream.fusion_law: stream fusion correctness axiom. Type: {Ξ± Ξ² Ξ³ : Type} β†’ (f : Ξ² β†’ Ξ³) β†’ (g : Ξ± β†’ Ξ²) β†’ s : Stream Ξ± β†’ Stream.map f (Stream.map g s) = Stream.map (f ∘ g) s
strm_ext_guarded_fix_ty
Stream.guarded_fix: guarded fixed point / corecursion under guard. Type: {Ξ± : Type} β†’ (Stream Ξ± β†’ Stream Ξ±) β†’ Stream Ξ±
strm_ext_kpn_channel_ty
KPN.channel: a Kahn process network channel (FIFO stream). Type: Type β†’ Type
strm_ext_kpn_process_ty
KPN.process: a Kahn process (reads inputs, writes outputs). Type: {Ξ± Ξ² : Type} β†’ Stream Ξ± β†’ Stream Ξ²
strm_ext_mealy_machine_ty
MealyMachine.type: a Mealy machine as stream transducer. Type: Type β†’ Type β†’ Type β†’ Type
strm_ext_mealy_run_ty
MealyMachine.run: run a Mealy machine on a stream of inputs. Type: {S I O : Type} β†’ MealyMachine S I O β†’ S β†’ Stream I β†’ Stream O
strm_ext_moore_machine_ty
MooreMachine.type: a Moore machine. Type: Type β†’ Type β†’ Type β†’ Type
strm_ext_productivity_ty
Stream.productivity: guardedness / productivity condition. Type: {Ξ± : Type} β†’ Stream Ξ± β†’ Prop
strm_ext_weighted_automaton_ty
WeightedAutomaton.type: weighted automaton over streams. Type: Type β†’ Type β†’ Type β†’ Type