| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (214 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (17 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (89 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (24 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (37 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (23 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
Global Index
A
abc [lemma, in StreamCalculus.math_stream]Abc [section, in StreamCalculus.math_stream]
abc_step1 [lemma, in StreamCalculus.math_stream]
Abc.T [variable, in StreamCalculus.math_stream]
Addition [section, in StreamCalculus.stream_addition]
addition_derive_up_to [lemma, in StreamCalculus.stream_addition]
addition_pointwise [lemma, in StreamCalculus.stream_addition]
addition_derive [lemma, in StreamCalculus.stream_addition]
add_both [lemma, in StreamCalculus.stream_addition]
C
cat [definition, in StreamCalculus.catalan]catalan [library]
CatalanStream [section, in StreamCalculus.catalan]
CatalanStream.T [variable, in StreamCalculus.catalan]
cat_char [lemma, in StreamCalculus.catalan]
cat' [definition, in StreamCalculus.catalan]
cat'' [lemma, in StreamCalculus.catalan]
Causality [section, in StreamCalculus.sde]
causality_inheritance [lemma, in StreamCalculus.sde]
Causality.T [variable, in StreamCalculus.sde]
causal_head [definition, in StreamCalculus.sde]
causal2 [definition, in StreamCalculus.sde]
cleaner_mult_derive [lemma, in StreamCalculus.conv_ring]
closed_cat [lemma, in StreamCalculus.catalan]
CommonLemma [section, in StreamCalculus.streamscommon]
CommonLemma.T [variable, in StreamCalculus.streamscommon]
ConvInverse [section, in StreamCalculus.conv_division]
ConvInverseProp [section, in StreamCalculus.conv_division]
ConvInverseProp.T [variable, in StreamCalculus.conv_division]
ConvInverse.T [variable, in StreamCalculus.conv_division]
ConvRingUpTo [instance, in StreamCalculus.conv_ring]
ConvRoot [section, in StreamCalculus.conv_sqrt]
ConvRoot.T [variable, in StreamCalculus.conv_sqrt]
conv_ring [lemma, in StreamCalculus.conv_ring_ring]
Conv_Ring.T [variable, in StreamCalculus.conv_ring_ring]
Conv_Ring [section, in StreamCalculus.conv_ring_ring]
conv_comm_monoid [instance, in StreamCalculus.conv_ring]
conv_assoc [lemma, in StreamCalculus.conv_ring]
conv_scalar [lemma, in StreamCalculus.conv_ring]
conv_comm [lemma, in StreamCalculus.conv_ring]
conv_left_identity [lemma, in StreamCalculus.conv_ring]
conv_left_absorb [lemma, in StreamCalculus.conv_ring]
conv_prod_proper [instance, in StreamCalculus.conv_ring]
conv_prod_proper_upto [instance, in StreamCalculus.conv_ring]
conv_prod_uptoproper [lemma, in StreamCalculus.conv_ring]
conv_sqrt [definition, in StreamCalculus.conv_sqrt]
conv_sqrt_tail_tail_causal [lemma, in StreamCalculus.conv_sqrt]
conv_sqrt_tail_tail [definition, in StreamCalculus.conv_sqrt]
conv_ainverse_cor [lemma, in StreamCalculus.conv_division]
conv_apreinverse_cor [lemma, in StreamCalculus.conv_division]
conv_ainverse [lemma, in StreamCalculus.conv_division]
conv_apreinverse [definition, in StreamCalculus.conv_division]
conv_proper [instance, in StreamCalculus.conv_division]
conv_proper_up_to [instance, in StreamCalculus.conv_division]
conv_inverse_cor [lemma, in StreamCalculus.conv_division]
conv_inverse_tail_cor [lemma, in StreamCalculus.conv_division]
conv_inverse [definition, in StreamCalculus.conv_division]
conv_inverse_tail_tail_cor [lemma, in StreamCalculus.conv_division]
conv_inverse_tail [definition, in StreamCalculus.conv_division]
conv_inverse_tail_tail_causal2 [lemma, in StreamCalculus.conv_division]
conv_inverse_tail_tail [definition, in StreamCalculus.conv_division]
conv_ring [library]
conv_division [library]
conv_ring_ring [library]
conv_sqrt [library]
corec [definition, in StreamCalculus.sde]
Corecursion [section, in StreamCalculus.sde]
Corecursion.T [variable, in StreamCalculus.sde]
Corecursion.X [variable, in StreamCalculus.sde]
corec_causal [lemma, in StreamCalculus.sde]
corec_tail [lemma, in StreamCalculus.sde]
corec_tail_up_to [lemma, in StreamCalculus.sde]
corec_up_to_eq_upton [lemma, in StreamCalculus.sde]
corec_up_to_tail [lemma, in StreamCalculus.sde]
corec_up_to_convergates [lemma, in StreamCalculus.sde]
corec_step_rewrite [lemma, in StreamCalculus.sde]
corec_head [lemma, in StreamCalculus.sde]
corec_up_to [definition, in StreamCalculus.sde]
D
derive [definition, in StreamCalculus.streamscommon]deriveProp [instance, in StreamCalculus.stream_equality]
deriveProper [instance, in StreamCalculus.conv_ring]
derive_rewrite [lemma, in StreamCalculus.streamscommon]
derive_X_upto [lemma, in StreamCalculus.conv_ring]
derive_X_id [lemma, in StreamCalculus.conv_ring]
derive_minus_upto [lemma, in StreamCalculus.stream_addition]
derive_X [lemma, in StreamCalculus.special_streams]
distribute_left [lemma, in StreamCalculus.conv_ring]
divide_right [lemma, in StreamCalculus.conv_division]
double_negation [lemma, in StreamCalculus.stream_addition]
E
equalO [constructor, in StreamCalculus.stream_equality_up_to]equalS [constructor, in StreamCalculus.stream_equality_up_to]
eqUpTo_lePointwise [lemma, in StreamCalculus.stream_equality_up_to]
eqUpTo_back [lemma, in StreamCalculus.stream_equality_up_to]
eqUpTo_trans [lemma, in StreamCalculus.stream_equality_up_to]
eqUpTo_symm [lemma, in StreamCalculus.stream_equality_up_to]
eqUpTo_refl [lemma, in StreamCalculus.stream_equality_up_to]
eqUpTo_inverse_tail [lemma, in StreamCalculus.stream_equality_up_to]
eqUpTo_inverse_head [lemma, in StreamCalculus.stream_equality_up_to]
eqUpTo_fromPointwise' [lemma, in StreamCalculus.conv_sqrt]
eqUpTo_fromPointwise [lemma, in StreamCalculus.stream_equalities]
eq_scalar_stream [lemma, in StreamCalculus.special_streams]
eq_derive [lemma, in StreamCalculus.stream_equality]
ex_inv [projection, in StreamCalculus.conv_division]
F
FibBasic [section, in StreamCalculus.fib_basic]FibBasic.T [variable, in StreamCalculus.fib_basic]
fibonacci [definition, in StreamCalculus.fib_basic]
fib_closed [lemma, in StreamCalculus.fib_basic]
fib_tail [lemma, in StreamCalculus.fib_basic]
fib_basic [library]
fundamental_theorem [lemma, in StreamCalculus.conv_ring]
I
id_test [lemma, in StreamCalculus.conv_ring]id_proper [instance, in StreamCalculus.conv_ring]
Inverse [record, in StreamCalculus.conv_division]
inv2 [definition, in StreamCalculus.conv_sqrt]
M
MathStream [section, in StreamCalculus.math_stream]MathStream.T [variable, in StreamCalculus.math_stream]
math_stream [library]
minusOne_squared [lemma, in StreamCalculus.conv_ring]
minusOne_squared' [lemma, in StreamCalculus.conv_sqrt]
minus_0 [lemma, in StreamCalculus.streamscommon]
minus_eq_minusOne [lemma, in StreamCalculus.conv_ring]
minus_one [lemma, in StreamCalculus.stream_addition]
minus_derive [lemma, in StreamCalculus.stream_addition]
move_minus [lemma, in StreamCalculus.conv_ring]
move_plus_right [lemma, in StreamCalculus.stream_addition]
N
nat_lt [definition, in StreamCalculus.streamscommon]nat_lt' [instance, in StreamCalculus.stream_equality_up_to]
neg_proper_upto [instance, in StreamCalculus.conv_ring]
neg_proper [instance, in StreamCalculus.conv_ring]
nullStream [definition, in StreamCalculus.special_streams]
nullStream_derive [lemma, in StreamCalculus.conv_ring]
nullStream_derive [lemma, in StreamCalculus.special_streams]
P
plusAssocUpTo [lemma, in StreamCalculus.stream_addition]plusProp [instance, in StreamCalculus.stream_addition]
plus_left_absorb [lemma, in StreamCalculus.conv_ring]
pointwise_multiply [lemma, in StreamCalculus.math_stream]
pre_sfc_tail_step [lemma, in StreamCalculus.sde]
properUpTo [instance, in StreamCalculus.stream_addition]
R
recursive_equality [lemma, in StreamCalculus.stream_equality]S
scalar_to_stream_upto [instance, in StreamCalculus.conv_ring]scalar_to_streamProper [instance, in StreamCalculus.conv_ring]
scalar_plus [lemma, in StreamCalculus.stream_addition]
scalar_derive_upto [lemma, in StreamCalculus.special_streams]
scalar_derive_null [lemma, in StreamCalculus.special_streams]
scalar_to_streamProp [instance, in StreamCalculus.special_streams]
scalar_to_stream [definition, in StreamCalculus.special_streams]
scalar0_is_nullStream [lemma, in StreamCalculus.special_streams]
sde [library]
SpecialStreams [section, in StreamCalculus.special_streams]
[ _ ] [notation, in StreamCalculus.special_streams]
special_streams [library]
sPlusProper [instance, in StreamCalculus.conv_ring]
SqrtUniqueness [section, in StreamCalculus.conv_sqrt]
SqrtUniqueness.T [variable, in StreamCalculus.conv_sqrt]
sqrt_uniqueness [lemma, in StreamCalculus.conv_sqrt]
sqrt_uniqueness_up_to [lemma, in StreamCalculus.conv_sqrt]
sqrt_cor [lemma, in StreamCalculus.conv_sqrt]
sqrt_tail_cor [lemma, in StreamCalculus.conv_sqrt]
sqrt_proper [instance, in StreamCalculus.conv_sqrt]
sqrt_derive_sqrt_tail [lemma, in StreamCalculus.conv_sqrt]
sqrt_tail_rewrite [lemma, in StreamCalculus.conv_sqrt]
sqrt_tail [definition, in StreamCalculus.conv_sqrt]
sqrt1 [lemma, in StreamCalculus.conv_sqrt]
sSetoid [instance, in StreamCalculus.conv_ring]
Stream [definition, in StreamCalculus.streamscommon]
streamAddition [instance, in StreamCalculus.stream_addition]
StreamConvProperties [section, in StreamCalculus.conv_ring]
StreamConvProperties.T [variable, in StreamCalculus.conv_ring]
streamEq [instance, in StreamCalculus.stream_equality]
StreamEqualities [section, in StreamCalculus.stream_equalities]
streamEquality [definition, in StreamCalculus.stream_equality]
StreamEquality [section, in StreamCalculus.stream_equality]
StreamEqualityUpTo [section, in StreamCalculus.stream_equality_up_to]
StreamEqualUpTo [inductive, in StreamCalculus.stream_equality_up_to]
streamEqualUpTo_inverse [lemma, in StreamCalculus.stream_equality_up_to]
streamEqualUpTo_streamEquality' [instance, in StreamCalculus.conv_ring]
streamEqualUpTo_streamEquality [lemma, in StreamCalculus.stream_equalities]
streamEq'' [instance, in StreamCalculus.special_streams]
streamMult [instance, in StreamCalculus.conv_ring]
streamNegate [instance, in StreamCalculus.stream_addition]
streamOne [instance, in StreamCalculus.stream_addition]
StreamPlusEquality [section, in StreamCalculus.stream_addition]
[ _ ] [notation, in StreamCalculus.stream_addition]
StreamPlusEqUpTo [section, in StreamCalculus.stream_addition]
[ _ ] [notation, in StreamCalculus.stream_addition]
StreamRing [instance, in StreamCalculus.conv_ring]
StreamRingConv [section, in StreamCalculus.conv_ring]
StreamRingConvUpTo [section, in StreamCalculus.conv_ring]
StreamRingConvUpTo.T [variable, in StreamCalculus.conv_ring]
Streams [section, in StreamCalculus.streamscommon]
streamscommon [library]
streamSetoid [instance, in StreamCalculus.stream_equality]
streamZero [instance, in StreamCalculus.special_streams]
stream_sum_conv_prod [lemma, in StreamCalculus.math_stream]
stream_sum [definition, in StreamCalculus.math_stream]
stream_add_semigroup' [lemma, in StreamCalculus.stream_addition]
stream_add_abgroup [instance, in StreamCalculus.stream_addition]
stream_add_group [instance, in StreamCalculus.stream_addition]
stream_add_monoid [instance, in StreamCalculus.stream_addition]
stream_add_semigroup [instance, in StreamCalculus.stream_addition]
stream_equality_up_to [library]
stream_addition [library]
stream_equalities [library]
stream_equality [library]
subRel [instance, in StreamCalculus.conv_ring]
s_eq_pointwise [lemma, in StreamCalculus.stream_equality]
U
UniqueSolutionSDE [section, in StreamCalculus.sde]UniqueSolutionSDE.T [variable, in StreamCalculus.sde]
UniqueSolutionSDE.X [variable, in StreamCalculus.sde]
upToEq [instance, in StreamCalculus.stream_equality_up_to]
upToSetoid [instance, in StreamCalculus.stream_equality_up_to]
X
X [definition, in StreamCalculus.special_streams]X_assoc [lemma, in StreamCalculus.conv_ring]
other
_ =- _ _ [notation, in StreamCalculus.stream_equality_up_to][ _ ] [notation, in StreamCalculus.special_streams]
Notation Index
S
[ _ ] [in StreamCalculus.special_streams][ _ ] [in StreamCalculus.stream_addition]
[ _ ] [in StreamCalculus.stream_addition]
other
_ =- _ _ [in StreamCalculus.stream_equality_up_to][ _ ] [in StreamCalculus.special_streams]
Variable Index
A
Abc.T [in StreamCalculus.math_stream]C
CatalanStream.T [in StreamCalculus.catalan]Causality.T [in StreamCalculus.sde]
CommonLemma.T [in StreamCalculus.streamscommon]
ConvInverseProp.T [in StreamCalculus.conv_division]
ConvInverse.T [in StreamCalculus.conv_division]
ConvRoot.T [in StreamCalculus.conv_sqrt]
Conv_Ring.T [in StreamCalculus.conv_ring_ring]
Corecursion.T [in StreamCalculus.sde]
Corecursion.X [in StreamCalculus.sde]
F
FibBasic.T [in StreamCalculus.fib_basic]M
MathStream.T [in StreamCalculus.math_stream]S
SqrtUniqueness.T [in StreamCalculus.conv_sqrt]StreamConvProperties.T [in StreamCalculus.conv_ring]
StreamRingConvUpTo.T [in StreamCalculus.conv_ring]
U
UniqueSolutionSDE.T [in StreamCalculus.sde]UniqueSolutionSDE.X [in StreamCalculus.sde]
Library Index
C
catalanconv_ring
conv_division
conv_ring_ring
conv_sqrt
F
fib_basicM
math_streamS
sdespecial_streams
streamscommon
stream_equality_up_to
stream_addition
stream_equalities
stream_equality
Lemma Index
A
abc [in StreamCalculus.math_stream]abc_step1 [in StreamCalculus.math_stream]
addition_derive_up_to [in StreamCalculus.stream_addition]
addition_pointwise [in StreamCalculus.stream_addition]
addition_derive [in StreamCalculus.stream_addition]
add_both [in StreamCalculus.stream_addition]
C
cat_char [in StreamCalculus.catalan]cat'' [in StreamCalculus.catalan]
causality_inheritance [in StreamCalculus.sde]
cleaner_mult_derive [in StreamCalculus.conv_ring]
closed_cat [in StreamCalculus.catalan]
conv_ring [in StreamCalculus.conv_ring_ring]
conv_assoc [in StreamCalculus.conv_ring]
conv_scalar [in StreamCalculus.conv_ring]
conv_comm [in StreamCalculus.conv_ring]
conv_left_identity [in StreamCalculus.conv_ring]
conv_left_absorb [in StreamCalculus.conv_ring]
conv_prod_uptoproper [in StreamCalculus.conv_ring]
conv_sqrt_tail_tail_causal [in StreamCalculus.conv_sqrt]
conv_ainverse_cor [in StreamCalculus.conv_division]
conv_apreinverse_cor [in StreamCalculus.conv_division]
conv_ainverse [in StreamCalculus.conv_division]
conv_inverse_cor [in StreamCalculus.conv_division]
conv_inverse_tail_cor [in StreamCalculus.conv_division]
conv_inverse_tail_tail_cor [in StreamCalculus.conv_division]
conv_inverse_tail_tail_causal2 [in StreamCalculus.conv_division]
corec_causal [in StreamCalculus.sde]
corec_tail [in StreamCalculus.sde]
corec_tail_up_to [in StreamCalculus.sde]
corec_up_to_eq_upton [in StreamCalculus.sde]
corec_up_to_tail [in StreamCalculus.sde]
corec_up_to_convergates [in StreamCalculus.sde]
corec_step_rewrite [in StreamCalculus.sde]
corec_head [in StreamCalculus.sde]
D
derive_rewrite [in StreamCalculus.streamscommon]derive_X_upto [in StreamCalculus.conv_ring]
derive_X_id [in StreamCalculus.conv_ring]
derive_minus_upto [in StreamCalculus.stream_addition]
derive_X [in StreamCalculus.special_streams]
distribute_left [in StreamCalculus.conv_ring]
divide_right [in StreamCalculus.conv_division]
double_negation [in StreamCalculus.stream_addition]
E
eqUpTo_lePointwise [in StreamCalculus.stream_equality_up_to]eqUpTo_back [in StreamCalculus.stream_equality_up_to]
eqUpTo_trans [in StreamCalculus.stream_equality_up_to]
eqUpTo_symm [in StreamCalculus.stream_equality_up_to]
eqUpTo_refl [in StreamCalculus.stream_equality_up_to]
eqUpTo_inverse_tail [in StreamCalculus.stream_equality_up_to]
eqUpTo_inverse_head [in StreamCalculus.stream_equality_up_to]
eqUpTo_fromPointwise' [in StreamCalculus.conv_sqrt]
eqUpTo_fromPointwise [in StreamCalculus.stream_equalities]
eq_scalar_stream [in StreamCalculus.special_streams]
eq_derive [in StreamCalculus.stream_equality]
F
fib_closed [in StreamCalculus.fib_basic]fib_tail [in StreamCalculus.fib_basic]
fundamental_theorem [in StreamCalculus.conv_ring]
I
id_test [in StreamCalculus.conv_ring]M
minusOne_squared [in StreamCalculus.conv_ring]minusOne_squared' [in StreamCalculus.conv_sqrt]
minus_0 [in StreamCalculus.streamscommon]
minus_eq_minusOne [in StreamCalculus.conv_ring]
minus_one [in StreamCalculus.stream_addition]
minus_derive [in StreamCalculus.stream_addition]
move_minus [in StreamCalculus.conv_ring]
move_plus_right [in StreamCalculus.stream_addition]
N
nullStream_derive [in StreamCalculus.conv_ring]nullStream_derive [in StreamCalculus.special_streams]
P
plusAssocUpTo [in StreamCalculus.stream_addition]plus_left_absorb [in StreamCalculus.conv_ring]
pointwise_multiply [in StreamCalculus.math_stream]
pre_sfc_tail_step [in StreamCalculus.sde]
R
recursive_equality [in StreamCalculus.stream_equality]S
scalar_plus [in StreamCalculus.stream_addition]scalar_derive_upto [in StreamCalculus.special_streams]
scalar_derive_null [in StreamCalculus.special_streams]
scalar0_is_nullStream [in StreamCalculus.special_streams]
sqrt_uniqueness [in StreamCalculus.conv_sqrt]
sqrt_uniqueness_up_to [in StreamCalculus.conv_sqrt]
sqrt_cor [in StreamCalculus.conv_sqrt]
sqrt_tail_cor [in StreamCalculus.conv_sqrt]
sqrt_derive_sqrt_tail [in StreamCalculus.conv_sqrt]
sqrt_tail_rewrite [in StreamCalculus.conv_sqrt]
sqrt1 [in StreamCalculus.conv_sqrt]
streamEqualUpTo_inverse [in StreamCalculus.stream_equality_up_to]
streamEqualUpTo_streamEquality [in StreamCalculus.stream_equalities]
stream_sum_conv_prod [in StreamCalculus.math_stream]
stream_add_semigroup' [in StreamCalculus.stream_addition]
s_eq_pointwise [in StreamCalculus.stream_equality]
X
X_assoc [in StreamCalculus.conv_ring]Constructor Index
E
equalO [in StreamCalculus.stream_equality_up_to]equalS [in StreamCalculus.stream_equality_up_to]
Inductive Index
S
StreamEqualUpTo [in StreamCalculus.stream_equality_up_to]Projection Index
E
ex_inv [in StreamCalculus.conv_division]Section Index
A
Abc [in StreamCalculus.math_stream]Addition [in StreamCalculus.stream_addition]
C
CatalanStream [in StreamCalculus.catalan]Causality [in StreamCalculus.sde]
CommonLemma [in StreamCalculus.streamscommon]
ConvInverse [in StreamCalculus.conv_division]
ConvInverseProp [in StreamCalculus.conv_division]
ConvRoot [in StreamCalculus.conv_sqrt]
Conv_Ring [in StreamCalculus.conv_ring_ring]
Corecursion [in StreamCalculus.sde]
F
FibBasic [in StreamCalculus.fib_basic]M
MathStream [in StreamCalculus.math_stream]S
SpecialStreams [in StreamCalculus.special_streams]SqrtUniqueness [in StreamCalculus.conv_sqrt]
StreamConvProperties [in StreamCalculus.conv_ring]
StreamEqualities [in StreamCalculus.stream_equalities]
StreamEquality [in StreamCalculus.stream_equality]
StreamEqualityUpTo [in StreamCalculus.stream_equality_up_to]
StreamPlusEquality [in StreamCalculus.stream_addition]
StreamPlusEqUpTo [in StreamCalculus.stream_addition]
StreamRingConv [in StreamCalculus.conv_ring]
StreamRingConvUpTo [in StreamCalculus.conv_ring]
Streams [in StreamCalculus.streamscommon]
U
UniqueSolutionSDE [in StreamCalculus.sde]Instance Index
C
ConvRingUpTo [in StreamCalculus.conv_ring]conv_comm_monoid [in StreamCalculus.conv_ring]
conv_prod_proper [in StreamCalculus.conv_ring]
conv_prod_proper_upto [in StreamCalculus.conv_ring]
conv_proper [in StreamCalculus.conv_division]
conv_proper_up_to [in StreamCalculus.conv_division]
D
deriveProp [in StreamCalculus.stream_equality]deriveProper [in StreamCalculus.conv_ring]
I
id_proper [in StreamCalculus.conv_ring]N
nat_lt' [in StreamCalculus.stream_equality_up_to]neg_proper_upto [in StreamCalculus.conv_ring]
neg_proper [in StreamCalculus.conv_ring]
P
plusProp [in StreamCalculus.stream_addition]properUpTo [in StreamCalculus.stream_addition]
S
scalar_to_stream_upto [in StreamCalculus.conv_ring]scalar_to_streamProper [in StreamCalculus.conv_ring]
scalar_to_streamProp [in StreamCalculus.special_streams]
sPlusProper [in StreamCalculus.conv_ring]
sqrt_proper [in StreamCalculus.conv_sqrt]
sSetoid [in StreamCalculus.conv_ring]
streamAddition [in StreamCalculus.stream_addition]
streamEq [in StreamCalculus.stream_equality]
streamEqualUpTo_streamEquality' [in StreamCalculus.conv_ring]
streamEq'' [in StreamCalculus.special_streams]
streamMult [in StreamCalculus.conv_ring]
streamNegate [in StreamCalculus.stream_addition]
streamOne [in StreamCalculus.stream_addition]
StreamRing [in StreamCalculus.conv_ring]
streamSetoid [in StreamCalculus.stream_equality]
streamZero [in StreamCalculus.special_streams]
stream_add_abgroup [in StreamCalculus.stream_addition]
stream_add_group [in StreamCalculus.stream_addition]
stream_add_monoid [in StreamCalculus.stream_addition]
stream_add_semigroup [in StreamCalculus.stream_addition]
subRel [in StreamCalculus.conv_ring]
U
upToEq [in StreamCalculus.stream_equality_up_to]upToSetoid [in StreamCalculus.stream_equality_up_to]
Definition Index
C
cat [in StreamCalculus.catalan]cat' [in StreamCalculus.catalan]
causal_head [in StreamCalculus.sde]
causal2 [in StreamCalculus.sde]
conv_sqrt [in StreamCalculus.conv_sqrt]
conv_sqrt_tail_tail [in StreamCalculus.conv_sqrt]
conv_apreinverse [in StreamCalculus.conv_division]
conv_inverse [in StreamCalculus.conv_division]
conv_inverse_tail [in StreamCalculus.conv_division]
conv_inverse_tail_tail [in StreamCalculus.conv_division]
corec [in StreamCalculus.sde]
corec_up_to [in StreamCalculus.sde]
D
derive [in StreamCalculus.streamscommon]F
fibonacci [in StreamCalculus.fib_basic]I
inv2 [in StreamCalculus.conv_sqrt]N
nat_lt [in StreamCalculus.streamscommon]nullStream [in StreamCalculus.special_streams]
S
scalar_to_stream [in StreamCalculus.special_streams]sqrt_tail [in StreamCalculus.conv_sqrt]
Stream [in StreamCalculus.streamscommon]
streamEquality [in StreamCalculus.stream_equality]
stream_sum [in StreamCalculus.math_stream]
X
X [in StreamCalculus.special_streams]Record Index
I
Inverse [in StreamCalculus.conv_division]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (214 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (17 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (89 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (24 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (37 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (23 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |