| 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 | (322 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 | (34 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 | (20 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 | (21 entries) |
| Axiom 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) |
| 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 | (20 entries) |
| 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 | (39 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 | (11 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 | (59 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 | (105 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 | (11 entries) |
Global Index
A
Acc_lt [lemma, in Prelude.Data.Nat]Acons [constructor, in Prelude.Data.Open]
All [library]
Anil [constructor, in Prelude.Data.Open]
append [definition, in Prelude.Data.Text]
append [definition, in Prelude.Data.Bytes]
Applicative [record, in Prelude.Control]
applicative_pure_map [projection, in Prelude.Control]
applicative_interchange [projection, in Prelude.Control]
applicative_homomorphism [projection, in Prelude.Control]
applicative_composition [projection, in Prelude.Control]
applicative_identity [projection, in Prelude.Control]
applicative_is_functor [projection, in Prelude.Control]
apply [projection, in Prelude.Control]
ask [projection, in Prelude.Control.Classes]
B
bind [projection, in Prelude.Control]bind_Proper [instance, in Prelude.Control]
bind_map [projection, in Prelude.Control]
bind_morphism [projection, in Prelude.Control]
bind_associativity [projection, in Prelude.Control]
bind_right_identity [projection, in Prelude.Control]
bind_left_identity [projection, in Prelude.Control]
bool_EquDec [instance, in Prelude.Data.Equality]
Byte [library]
bytes [record, in Prelude.Data.Bytes]
Bytes [library]
bytes_of_text [definition, in Prelude.Data.Text]
bytes_of_wchar [definition, in Prelude.Data.Text]
bytes_of_list_byte_fmt [definition, in Prelude.Data.Bytes]
bytes_EquDec [instance, in Prelude.Data.Bytes]
bytes_Equality [instance, in Prelude.Data.Bytes]
bytes_equal_Equivalence [instance, in Prelude.Data.Bytes]
bytes_equal [definition, in Prelude.Data.Bytes]
bytes_of_int [definition, in Prelude.Data.Int]
bytes_of_byte [definition, in Prelude.Data.Byte]
byte_EquDec [instance, in Prelude.Data.Equality]
byte_equb_correct [axiom, in Prelude.Data.Equality]
byte_equb [definition, in Prelude.Data.Equality]
byte_of_bytes_fmt [definition, in Prelude.Data.Byte]
C
cardinal [definition, in Prelude.Data.Open]Classes [library]
compose [definition, in Prelude.Control]
Contains [record, in Prelude.Data.Open]
Contains_tail [instance, in Prelude.Data.Open]
Contains_head [instance, in Prelude.Data.Open]
Contains_nat [instance, in Prelude.Data.Open]
Control [library]
D
default_Equality [instance, in Prelude.Data.Equality]digit_of_wchar [definition, in Prelude.Data.Z]
digit_of_wchar [definition, in Prelude.Data.Int]
E
equal [projection, in Prelude.Data.Equality]equalb [projection, in Prelude.Data.Equality]
equalb_false_equ [lemma, in Prelude.Data.Equality]
equalb_equ_false [lemma, in Prelude.Data.Equality]
equalb_equ_true [projection, in Prelude.Data.Equality]
Equality [record, in Prelude.Data.Equality]
Equality [library]
equal_right [constructor, in Prelude.Control.Sum]
equal_left [constructor, in Prelude.Control.Sum]
EquDec [record, in Prelude.Data.Equality]
eval_state_t [definition, in Prelude.Control.State]
exec_state_t [definition, in Prelude.Control.State]
F
fconst [definition, in Prelude.Control]fetch [definition, in Prelude.Data.Open]
fromMaybe [definition, in Prelude.Control.Option]
fst_tuple_equal_Proper [instance, in Prelude.Data.Equality]
func [definition, in Prelude.Control.Function]
Function [library]
function_Equality [instance, in Prelude.Data.Equality]
Functor [record, in Prelude.Control]
functor_map_identity [projection, in Prelude.Control]
functor_identity [projection, in Prelude.Control]
functor_has_eq [projection, in Prelude.Control]
func_Monad [instance, in Prelude.Control.Function]
func_bind [definition, in Prelude.Control.Function]
func_Applicative [instance, in Prelude.Control.Function]
func_pure [definition, in Prelude.Control.Function]
func_apply [definition, in Prelude.Control.Function]
func_Functor [instance, in Prelude.Control.Function]
G
get [definition, in Prelude.Data.Open]get [projection, in Prelude.Control.Classes]
gets [definition, in Prelude.Control.Classes]
I
id [definition, in Prelude.Control]Identity [library]
identity_Monad [instance, in Prelude.Control.Identity]
identity_bind [definition, in Prelude.Control.Identity]
identity_Applicative [instance, in Prelude.Control.Identity]
identity_pure [definition, in Prelude.Control.Identity]
identity_apply [definition, in Prelude.Control.Identity]
identity_Functor [instance, in Prelude.Control.Identity]
identity_map [definition, in Prelude.Control.Identity]
identity_equal [definition, in Prelude.Control.Identity]
id_Equality [instance, in Prelude.Control.Identity]
Init [library]
inj [definition, in Prelude.Data.Open]
Int [library]
int_EquDec [instance, in Prelude.Data.Equality]
int_of_bytes [definition, in Prelude.Data.Int]
int_of_text [definition, in Prelude.Data.Int]
int_of_text_aux [definition, in Prelude.Data.Int]
int_div_lt [lemma, in Prelude.Data.Int]
int_lt_false_spec [axiom, in Prelude.Data.Int]
int_of_byte [definition, in Prelude.Data.Byte]
is_some_dec [definition, in Prelude.Control.Option]
is_some_rule [constructor, in Prelude.Control.Option]
is_some [inductive, in Prelude.Control.Option]
J
join [definition, in Prelude.Control]L
le [inductive, in Prelude.Data.Nat]le [definition, in Prelude.Data.Int]
length [definition, in Prelude.Data.Bytes]
length_nat [definition, in Prelude.Data.Bytes]
le_trans [lemma, in Prelude.Data.Nat]
le_succ_n_succ_m_le_n_m [lemma, in Prelude.Data.Nat]
le_trans_succ [lemma, in Prelude.Data.Nat]
le_n_succ_n [lemma, in Prelude.Data.Nat]
le_succ [constructor, in Prelude.Data.Nat]
le_refl [constructor, in Prelude.Data.Nat]
lift [projection, in Prelude.Control.Classes]
liftA2 [definition, in Prelude.Control]
list_EquDec [instance, in Prelude.Data.Equality]
list_equal_dec [definition, in Prelude.Data.Equality]
list_Equality [instance, in Prelude.Data.Equality]
list_equal_nil [constructor, in Prelude.Data.Equality]
list_equal_cons [constructor, in Prelude.Data.Equality]
list_equal [inductive, in Prelude.Data.Equality]
list_byte_of_text [definition, in Prelude.Data.Text]
list_byte_of_wchar [definition, in Prelude.Data.Text]
list_byte_of_list_byte_fmt [definition, in Prelude.Data.Bytes]
lseq [definition, in Prelude.Control]
lt [definition, in Prelude.Data.Nat]
lt [definition, in Prelude.Data.Int]
lt_wf [lemma, in Prelude.Data.Nat]
lt_not_refl [lemma, in Prelude.Data.Nat]
M
map [projection, in Prelude.Control]map_func [definition, in Prelude.Control.Function]
maybe [definition, in Prelude.Control.Option]
modify [definition, in Prelude.Control.Classes]
Monad [record, in Prelude.Control]
MonadReader [record, in Prelude.Control.Classes]
monadreader_is_monad [projection, in Prelude.Control.Classes]
MonadState [record, in Prelude.Control.Classes]
monadstate_is_monad [projection, in Prelude.Control.Classes]
MonadTrans [record, in Prelude.Control.Classes]
monadtransform_reader [instance, in Prelude.Control.Classes]
monadtransform_state [instance, in Prelude.Control.Classes]
monad_is_apply [projection, in Prelude.Control]
monad_trans_is_monad [projection, in Prelude.Control.Classes]
N
Nat [record, in Prelude.Data.Nat]Nat [library]
nat_EquDec [instance, in Prelude.Data.Equality]
nat_Nat [instance, in Prelude.Data.Nat]
not_equal_Symmetric [instance, in Prelude.Data.Equality]
not_equal_sym [lemma, in Prelude.Data.Equality]
not_le_succ_n_n [lemma, in Prelude.Data.Nat]
not_le_succ_n_zero [lemma, in Prelude.Data.Nat]
N_Nat [instance, in Prelude.Data.Nat]
O
OneOf [constructor, in Prelude.Data.Open]Open [library]
Option [library]
option_Monad [instance, in Prelude.Control.Option]
option_bind [definition, in Prelude.Control.Option]
option_Applicative [instance, in Prelude.Control.Option]
option_app [definition, in Prelude.Control.Option]
option_Functor [instance, in Prelude.Control.Option]
option_Equality [instance, in Prelude.Data.Equality]
option_equal_none [constructor, in Prelude.Data.Equality]
option_equal_some [constructor, in Prelude.Data.Equality]
option_equal [inductive, in Prelude.Data.Equality]
P
pair_tuple_equal_Proper [instance, in Prelude.Data.Equality]peano_rect [projection, in Prelude.Data.Nat]
product [inductive, in Prelude.Data.Open]
pure [projection, in Prelude.Control]
put [projection, in Prelude.Control.Classes]
R
rank [projection, in Prelude.Data.Open]rank_bound [projection, in Prelude.Data.Open]
rank_get_t [projection, in Prelude.Data.Open]
reader [definition, in Prelude.Control.Reader]
Reader [library]
reader_MonadReader [instance, in Prelude.Control.Reader]
reader_Monad [instance, in Prelude.Control.Reader]
reader_bind [definition, in Prelude.Control.Reader]
reader_Applicative [instance, in Prelude.Control.Reader]
reader_apply [definition, in Prelude.Control.Reader]
reader_pure [definition, in Prelude.Control.Reader]
reader_Functor [instance, in Prelude.Control.Reader]
reader_map [definition, in Prelude.Control.Reader]
reader_t [definition, in Prelude.Control.Reader]
read_wchar [definition, in Prelude.Data.Text]
rel [projection, in Prelude.Data.Equality]
remove [definition, in Prelude.Data.Open]
rseq [definition, in Prelude.Control]
run_state_t [definition, in Prelude.Control.State]
S
sigma_EquDec [instance, in Prelude.Data.Equality]sigma_Equality [instance, in Prelude.Data.Equality]
snd_tuple_equal_Proper [instance, in Prelude.Data.Equality]
some_equal_Proper [instance, in Prelude.Data.Equality]
state [definition, in Prelude.Control.State]
State [library]
state_StateMonad [instance, in Prelude.Control.State]
state_put [definition, in Prelude.Control.State]
state_get [definition, in Prelude.Control.State]
state_MonadTrans [instance, in Prelude.Control.State]
state_lift [definition, in Prelude.Control.State]
state_Monad [instance, in Prelude.Control.State]
state_bind_associativity [lemma, in Prelude.Control.State]
state_bind [definition, in Prelude.Control.State]
state_Applicative [instance, in Prelude.Control.State]
state_applicative_interchange [lemma, in Prelude.Control.State]
state_applicative_homomorphism [lemma, in Prelude.Control.State]
state_applicative_identity [lemma, in Prelude.Control.State]
state_pure [definition, in Prelude.Control.State]
state_apply [definition, in Prelude.Control.State]
state_Functor [instance, in Prelude.Control.State]
state_functor_composition_identity [lemma, in Prelude.Control.State]
state_functor_identity [lemma, in Prelude.Control.State]
state_map [definition, in Prelude.Control.State]
state_t [definition, in Prelude.Control.State]
string_EquDec [instance, in Prelude.Data.Equality]
succ [projection, in Prelude.Data.Nat]
succ_n_neq_n [lemma, in Prelude.Data.Nat]
succ_not_zero [projection, in Prelude.Data.Nat]
succ_injective [projection, in Prelude.Data.Nat]
Sum [library]
sum_Monad [instance, in Prelude.Control.Sum]
sum_bind [definition, in Prelude.Control.Sum]
sum_Applicative [instance, in Prelude.Control.Sum]
sum_app [definition, in Prelude.Control.Sum]
sum_pure [definition, in Prelude.Control.Sum]
sum_Functor [instance, in Prelude.Control.Sum]
sum_map [definition, in Prelude.Control.Sum]
sum_Equality [instance, in Prelude.Control.Sum]
sum_equal_Equivalence [instance, in Prelude.Control.Sum]
sum_equal [inductive, in Prelude.Control.Sum]
swap [definition, in Prelude.Data.Open]
T
Tactics [library]TCons [constructor, in Prelude.Data.Text]
test_monad_notation [definition, in Prelude.Control]
text [inductive, in Prelude.Data.Text]
Text [library]
text_of_Z [definition, in Prelude.Data.Z]
text_of_Z_aux [definition, in Prelude.Data.Z]
text_of_list_byte_fmt [definition, in Prelude.Data.Text]
text_of_text_fmt [definition, in Prelude.Data.Text]
text_length [definition, in Prelude.Data.Text]
text_length_nat [definition, in Prelude.Data.Text]
text_size [definition, in Prelude.Data.Text]
text_size_nat [definition, in Prelude.Data.Text]
text_EquDec [instance, in Prelude.Data.Text]
text_eqb [definition, in Prelude.Data.Text]
text_Equality [instance, in Prelude.Data.Text]
text_equal_Equivalence [instance, in Prelude.Data.Text]
text_equal_tnil [constructor, in Prelude.Data.Text]
text_equal_tcons [constructor, in Prelude.Data.Text]
text_equal [inductive, in Prelude.Data.Text]
text_of_bytes [definition, in Prelude.Data.Text]
text_of_list_byte [definition, in Prelude.Data.Text]
text_of_int [definition, in Prelude.Data.Int]
text_of_int_aux [definition, in Prelude.Data.Int]
TNil [constructor, in Prelude.Data.Text]
tuple_EquDec [instance, in Prelude.Data.Equality]
tuple_Equality [instance, in Prelude.Data.Equality]
U
union [inductive, in Prelude.Data.Open]unwrap_bytes [projection, in Prelude.Data.Bytes]
V
visit [definition, in Prelude.Data.Open]void [definition, in Prelude.Control]
Void [inductive, in Prelude.Data.Void]
Void [library]
W
wchar [inductive, in Prelude.Data.Text]wchar_of_digit [definition, in Prelude.Data.Z]
wchar_of_list_byte_fmt [definition, in Prelude.Data.Text]
wchar_of_bytes [definition, in Prelude.Data.Text]
wchar_of_list_byte [definition, in Prelude.Data.Text]
wchar_EquDec [instance, in Prelude.Data.Text]
wchar_eqb [definition, in Prelude.Data.Text]
wchar_size [definition, in Prelude.Data.Text]
wchar_size_nat [definition, in Prelude.Data.Text]
wchar_var_4 [constructor, in Prelude.Data.Text]
wchar_var_3 [constructor, in Prelude.Data.Text]
wchar_var_2 [constructor, in Prelude.Data.Text]
wchar_var_1 [constructor, in Prelude.Data.Text]
wchar_of_digit [definition, in Prelude.Data.Int]
when [definition, in Prelude.Control]
wrap_bytes [constructor, in Prelude.Data.Bytes]
Z
Z [library]zero [projection, in Prelude.Data.Nat]
Z_of_text [definition, in Prelude.Data.Z]
Z_of_text_aux [definition, in Prelude.Data.Z]
Z_EquDec [instance, in Prelude.Data.Equality]
other
monad:_ [notation, in Prelude.Control]monad:_ ; _ [notation, in Prelude.Control]
monad:let _ := _ in _ [notation, in Prelude.Control]
monad:let* _ := _ in _ [notation, in Prelude.Control]
_ ++ _ (bytes_scope) [notation, in Prelude.Data.Bytes]
fun* _ .. _ => _ (function_scope) [notation, in Prelude.Control]
_ >>> _ (function_scope) [notation, in Prelude.Control]
_ <<< _ (function_scope) [notation, in Prelude.Control]
_ <=? _ (int63_scope) [notation, in Prelude.Data.Int]
_ [notation, in Prelude.Data.Int]
_ <= _ (int63_scope) [notation, in Prelude.Data.Int]
_ < _ (int63_scope) [notation, in Prelude.Data.Int]
_ >>= _ (monad_scope) [notation, in Prelude.Control]
_ <* _ (monad_scope) [notation, in Prelude.Control]
_ *> _ (monad_scope) [notation, in Prelude.Control]
_ <*> _ (monad_scope) [notation, in Prelude.Control]
_ <$ _ (monad_scope) [notation, in Prelude.Control]
_ <$> _ (monad_scope) [notation, in Prelude.Control]
_ > _ (Nat_scope) [notation, in Prelude.Data.Nat]
_ < _ (Nat_scope) [notation, in Prelude.Data.Nat]
_ >= _ (Nat_scope) [notation, in Prelude.Data.Nat]
_ <= _ (Nat_scope) [notation, in Prelude.Data.Nat]
do _ end (prelude_scope) [notation, in Prelude.Control]
_ $ _ (prelude_scope) [notation, in Prelude.Control]
_ ?/= _ (prelude_scope) [notation, in Prelude.Data.Equality]
_ ?= _ (prelude_scope) [notation, in Prelude.Data.Equality]
_ /= _ (prelude_scope) [notation, in Prelude.Data.Equality]
_ == _ (prelude_scope) [notation, in Prelude.Data.Equality]
'equal (prelude_scope) [notation, in Prelude.Data.Equality]
t# _ (prelude_scope) [notation, in Prelude.Data.Text]
w# _ (prelude_scope) [notation, in Prelude.Data.Text]
b# _ (prelude_scope) [notation, in Prelude.Data.Bytes]
c# _ (prelude_scope) [notation, in Prelude.Data.Byte]
_ ++ _ (text_scope) [notation, in Prelude.Data.Text]
Notation Index
other
monad:_ [in Prelude.Control]monad:_ ; _ [in Prelude.Control]
monad:let _ := _ in _ [in Prelude.Control]
monad:let* _ := _ in _ [in Prelude.Control]
_ ++ _ (bytes_scope) [in Prelude.Data.Bytes]
fun* _ .. _ => _ (function_scope) [in Prelude.Control]
_ >>> _ (function_scope) [in Prelude.Control]
_ <<< _ (function_scope) [in Prelude.Control]
_ <=? _ (int63_scope) [in Prelude.Data.Int]
_ [in Prelude.Data.Int]
_ <= _ (int63_scope) [in Prelude.Data.Int]
_ < _ (int63_scope) [in Prelude.Data.Int]
_ >>= _ (monad_scope) [in Prelude.Control]
_ <* _ (monad_scope) [in Prelude.Control]
_ *> _ (monad_scope) [in Prelude.Control]
_ <*> _ (monad_scope) [in Prelude.Control]
_ <$ _ (monad_scope) [in Prelude.Control]
_ <$> _ (monad_scope) [in Prelude.Control]
_ > _ (Nat_scope) [in Prelude.Data.Nat]
_ < _ (Nat_scope) [in Prelude.Data.Nat]
_ >= _ (Nat_scope) [in Prelude.Data.Nat]
_ <= _ (Nat_scope) [in Prelude.Data.Nat]
do _ end (prelude_scope) [in Prelude.Control]
_ $ _ (prelude_scope) [in Prelude.Control]
_ ?/= _ (prelude_scope) [in Prelude.Data.Equality]
_ ?= _ (prelude_scope) [in Prelude.Data.Equality]
_ /= _ (prelude_scope) [in Prelude.Data.Equality]
_ == _ (prelude_scope) [in Prelude.Data.Equality]
'equal (prelude_scope) [in Prelude.Data.Equality]
t# _ (prelude_scope) [in Prelude.Data.Text]
w# _ (prelude_scope) [in Prelude.Data.Text]
b# _ (prelude_scope) [in Prelude.Data.Bytes]
c# _ (prelude_scope) [in Prelude.Data.Byte]
_ ++ _ (text_scope) [in Prelude.Data.Text]
Library Index
A
AllB
ByteBytes
C
ClassesControl
E
EqualityF
FunctionI
IdentityInit
Int
N
NatO
OpenOption
R
ReaderS
StateSum
T
TacticsText
V
VoidZ
ZConstructor Index
A
Acons [in Prelude.Data.Open]Anil [in Prelude.Data.Open]
E
equal_right [in Prelude.Control.Sum]equal_left [in Prelude.Control.Sum]
I
is_some_rule [in Prelude.Control.Option]L
le_succ [in Prelude.Data.Nat]le_refl [in Prelude.Data.Nat]
list_equal_nil [in Prelude.Data.Equality]
list_equal_cons [in Prelude.Data.Equality]
O
OneOf [in Prelude.Data.Open]option_equal_none [in Prelude.Data.Equality]
option_equal_some [in Prelude.Data.Equality]
T
TCons [in Prelude.Data.Text]text_equal_tnil [in Prelude.Data.Text]
text_equal_tcons [in Prelude.Data.Text]
TNil [in Prelude.Data.Text]
W
wchar_var_4 [in Prelude.Data.Text]wchar_var_3 [in Prelude.Data.Text]
wchar_var_2 [in Prelude.Data.Text]
wchar_var_1 [in Prelude.Data.Text]
wrap_bytes [in Prelude.Data.Bytes]
Axiom Index
B
byte_equb_correct [in Prelude.Data.Equality]I
int_lt_false_spec [in Prelude.Data.Int]Lemma Index
A
Acc_lt [in Prelude.Data.Nat]E
equalb_false_equ [in Prelude.Data.Equality]equalb_equ_false [in Prelude.Data.Equality]
I
int_div_lt [in Prelude.Data.Int]L
le_trans [in Prelude.Data.Nat]le_succ_n_succ_m_le_n_m [in Prelude.Data.Nat]
le_trans_succ [in Prelude.Data.Nat]
le_n_succ_n [in Prelude.Data.Nat]
lt_wf [in Prelude.Data.Nat]
lt_not_refl [in Prelude.Data.Nat]
N
not_equal_sym [in Prelude.Data.Equality]not_le_succ_n_n [in Prelude.Data.Nat]
not_le_succ_n_zero [in Prelude.Data.Nat]
S
state_bind_associativity [in Prelude.Control.State]state_applicative_interchange [in Prelude.Control.State]
state_applicative_homomorphism [in Prelude.Control.State]
state_applicative_identity [in Prelude.Control.State]
state_functor_composition_identity [in Prelude.Control.State]
state_functor_identity [in Prelude.Control.State]
succ_n_neq_n [in Prelude.Data.Nat]
Projection Index
A
applicative_pure_map [in Prelude.Control]applicative_interchange [in Prelude.Control]
applicative_homomorphism [in Prelude.Control]
applicative_composition [in Prelude.Control]
applicative_identity [in Prelude.Control]
applicative_is_functor [in Prelude.Control]
apply [in Prelude.Control]
ask [in Prelude.Control.Classes]
B
bind [in Prelude.Control]bind_map [in Prelude.Control]
bind_morphism [in Prelude.Control]
bind_associativity [in Prelude.Control]
bind_right_identity [in Prelude.Control]
bind_left_identity [in Prelude.Control]
E
equal [in Prelude.Data.Equality]equalb [in Prelude.Data.Equality]
equalb_equ_true [in Prelude.Data.Equality]
F
functor_map_identity [in Prelude.Control]functor_identity [in Prelude.Control]
functor_has_eq [in Prelude.Control]
G
get [in Prelude.Control.Classes]L
lift [in Prelude.Control.Classes]M
map [in Prelude.Control]monadreader_is_monad [in Prelude.Control.Classes]
monadstate_is_monad [in Prelude.Control.Classes]
monad_is_apply [in Prelude.Control]
monad_trans_is_monad [in Prelude.Control.Classes]
P
peano_rect [in Prelude.Data.Nat]pure [in Prelude.Control]
put [in Prelude.Control.Classes]
R
rank [in Prelude.Data.Open]rank_bound [in Prelude.Data.Open]
rank_get_t [in Prelude.Data.Open]
rel [in Prelude.Data.Equality]
S
succ [in Prelude.Data.Nat]succ_not_zero [in Prelude.Data.Nat]
succ_injective [in Prelude.Data.Nat]
U
unwrap_bytes [in Prelude.Data.Bytes]Z
zero [in Prelude.Data.Nat]Inductive Index
I
is_some [in Prelude.Control.Option]L
le [in Prelude.Data.Nat]list_equal [in Prelude.Data.Equality]
O
option_equal [in Prelude.Data.Equality]P
product [in Prelude.Data.Open]S
sum_equal [in Prelude.Control.Sum]T
text [in Prelude.Data.Text]text_equal [in Prelude.Data.Text]
U
union [in Prelude.Data.Open]V
Void [in Prelude.Data.Void]W
wchar [in Prelude.Data.Text]Instance Index
B
bind_Proper [in Prelude.Control]bool_EquDec [in Prelude.Data.Equality]
bytes_EquDec [in Prelude.Data.Bytes]
bytes_Equality [in Prelude.Data.Bytes]
bytes_equal_Equivalence [in Prelude.Data.Bytes]
byte_EquDec [in Prelude.Data.Equality]
C
Contains_tail [in Prelude.Data.Open]Contains_head [in Prelude.Data.Open]
Contains_nat [in Prelude.Data.Open]
D
default_Equality [in Prelude.Data.Equality]F
fst_tuple_equal_Proper [in Prelude.Data.Equality]function_Equality [in Prelude.Data.Equality]
func_Monad [in Prelude.Control.Function]
func_Applicative [in Prelude.Control.Function]
func_Functor [in Prelude.Control.Function]
I
identity_Monad [in Prelude.Control.Identity]identity_Applicative [in Prelude.Control.Identity]
identity_Functor [in Prelude.Control.Identity]
id_Equality [in Prelude.Control.Identity]
int_EquDec [in Prelude.Data.Equality]
L
list_EquDec [in Prelude.Data.Equality]list_Equality [in Prelude.Data.Equality]
M
monadtransform_reader [in Prelude.Control.Classes]monadtransform_state [in Prelude.Control.Classes]
N
nat_EquDec [in Prelude.Data.Equality]nat_Nat [in Prelude.Data.Nat]
not_equal_Symmetric [in Prelude.Data.Equality]
N_Nat [in Prelude.Data.Nat]
O
option_Monad [in Prelude.Control.Option]option_Applicative [in Prelude.Control.Option]
option_Functor [in Prelude.Control.Option]
option_Equality [in Prelude.Data.Equality]
P
pair_tuple_equal_Proper [in Prelude.Data.Equality]R
reader_MonadReader [in Prelude.Control.Reader]reader_Monad [in Prelude.Control.Reader]
reader_Applicative [in Prelude.Control.Reader]
reader_Functor [in Prelude.Control.Reader]
S
sigma_EquDec [in Prelude.Data.Equality]sigma_Equality [in Prelude.Data.Equality]
snd_tuple_equal_Proper [in Prelude.Data.Equality]
some_equal_Proper [in Prelude.Data.Equality]
state_StateMonad [in Prelude.Control.State]
state_MonadTrans [in Prelude.Control.State]
state_Monad [in Prelude.Control.State]
state_Applicative [in Prelude.Control.State]
state_Functor [in Prelude.Control.State]
string_EquDec [in Prelude.Data.Equality]
sum_Monad [in Prelude.Control.Sum]
sum_Applicative [in Prelude.Control.Sum]
sum_Functor [in Prelude.Control.Sum]
sum_Equality [in Prelude.Control.Sum]
sum_equal_Equivalence [in Prelude.Control.Sum]
T
text_EquDec [in Prelude.Data.Text]text_Equality [in Prelude.Data.Text]
text_equal_Equivalence [in Prelude.Data.Text]
tuple_EquDec [in Prelude.Data.Equality]
tuple_Equality [in Prelude.Data.Equality]
W
wchar_EquDec [in Prelude.Data.Text]Z
Z_EquDec [in Prelude.Data.Equality]Definition Index
A
append [in Prelude.Data.Text]append [in Prelude.Data.Bytes]
B
bytes_of_text [in Prelude.Data.Text]bytes_of_wchar [in Prelude.Data.Text]
bytes_of_list_byte_fmt [in Prelude.Data.Bytes]
bytes_equal [in Prelude.Data.Bytes]
bytes_of_int [in Prelude.Data.Int]
bytes_of_byte [in Prelude.Data.Byte]
byte_equb [in Prelude.Data.Equality]
byte_of_bytes_fmt [in Prelude.Data.Byte]
C
cardinal [in Prelude.Data.Open]compose [in Prelude.Control]
D
digit_of_wchar [in Prelude.Data.Z]digit_of_wchar [in Prelude.Data.Int]
E
eval_state_t [in Prelude.Control.State]exec_state_t [in Prelude.Control.State]
F
fconst [in Prelude.Control]fetch [in Prelude.Data.Open]
fromMaybe [in Prelude.Control.Option]
func [in Prelude.Control.Function]
func_bind [in Prelude.Control.Function]
func_pure [in Prelude.Control.Function]
func_apply [in Prelude.Control.Function]
G
get [in Prelude.Data.Open]gets [in Prelude.Control.Classes]
I
id [in Prelude.Control]identity_bind [in Prelude.Control.Identity]
identity_pure [in Prelude.Control.Identity]
identity_apply [in Prelude.Control.Identity]
identity_map [in Prelude.Control.Identity]
identity_equal [in Prelude.Control.Identity]
inj [in Prelude.Data.Open]
int_of_bytes [in Prelude.Data.Int]
int_of_text [in Prelude.Data.Int]
int_of_text_aux [in Prelude.Data.Int]
int_of_byte [in Prelude.Data.Byte]
is_some_dec [in Prelude.Control.Option]
J
join [in Prelude.Control]L
le [in Prelude.Data.Int]length [in Prelude.Data.Bytes]
length_nat [in Prelude.Data.Bytes]
liftA2 [in Prelude.Control]
list_equal_dec [in Prelude.Data.Equality]
list_byte_of_text [in Prelude.Data.Text]
list_byte_of_wchar [in Prelude.Data.Text]
list_byte_of_list_byte_fmt [in Prelude.Data.Bytes]
lseq [in Prelude.Control]
lt [in Prelude.Data.Nat]
lt [in Prelude.Data.Int]
M
map_func [in Prelude.Control.Function]maybe [in Prelude.Control.Option]
modify [in Prelude.Control.Classes]
O
option_bind [in Prelude.Control.Option]option_app [in Prelude.Control.Option]
R
reader [in Prelude.Control.Reader]reader_bind [in Prelude.Control.Reader]
reader_apply [in Prelude.Control.Reader]
reader_pure [in Prelude.Control.Reader]
reader_map [in Prelude.Control.Reader]
reader_t [in Prelude.Control.Reader]
read_wchar [in Prelude.Data.Text]
remove [in Prelude.Data.Open]
rseq [in Prelude.Control]
run_state_t [in Prelude.Control.State]
S
state [in Prelude.Control.State]state_put [in Prelude.Control.State]
state_get [in Prelude.Control.State]
state_lift [in Prelude.Control.State]
state_bind [in Prelude.Control.State]
state_pure [in Prelude.Control.State]
state_apply [in Prelude.Control.State]
state_map [in Prelude.Control.State]
state_t [in Prelude.Control.State]
sum_bind [in Prelude.Control.Sum]
sum_app [in Prelude.Control.Sum]
sum_pure [in Prelude.Control.Sum]
sum_map [in Prelude.Control.Sum]
swap [in Prelude.Data.Open]
T
test_monad_notation [in Prelude.Control]text_of_Z [in Prelude.Data.Z]
text_of_Z_aux [in Prelude.Data.Z]
text_of_list_byte_fmt [in Prelude.Data.Text]
text_of_text_fmt [in Prelude.Data.Text]
text_length [in Prelude.Data.Text]
text_length_nat [in Prelude.Data.Text]
text_size [in Prelude.Data.Text]
text_size_nat [in Prelude.Data.Text]
text_eqb [in Prelude.Data.Text]
text_of_bytes [in Prelude.Data.Text]
text_of_list_byte [in Prelude.Data.Text]
text_of_int [in Prelude.Data.Int]
text_of_int_aux [in Prelude.Data.Int]
V
visit [in Prelude.Data.Open]void [in Prelude.Control]
W
wchar_of_digit [in Prelude.Data.Z]wchar_of_list_byte_fmt [in Prelude.Data.Text]
wchar_of_bytes [in Prelude.Data.Text]
wchar_of_list_byte [in Prelude.Data.Text]
wchar_eqb [in Prelude.Data.Text]
wchar_size [in Prelude.Data.Text]
wchar_size_nat [in Prelude.Data.Text]
wchar_of_digit [in Prelude.Data.Int]
when [in Prelude.Control]
Z
Z_of_text [in Prelude.Data.Z]Z_of_text_aux [in Prelude.Data.Z]
Record Index
A
Applicative [in Prelude.Control]B
bytes [in Prelude.Data.Bytes]C
Contains [in Prelude.Data.Open]E
Equality [in Prelude.Data.Equality]EquDec [in Prelude.Data.Equality]
F
Functor [in Prelude.Control]M
Monad [in Prelude.Control]MonadReader [in Prelude.Control.Classes]
MonadState [in Prelude.Control.Classes]
MonadTrans [in Prelude.Control.Classes]
N
Nat [in Prelude.Data.Nat]| 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 | (322 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 | (34 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 | (20 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 | (21 entries) |
| Axiom 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) |
| 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 | (20 entries) |
| 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 | (39 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 | (11 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 | (59 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 | (105 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 | (11 entries) |
This page has been generated by coqdoc