| 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 | (799 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 | (37 entries) |
| Module 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 | (32 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 | (171 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 | (23 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 | (117 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) |
| 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 | (261 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 | (1 entry) |
| 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 | (6 entries) |
| 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 | (26 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 | (2 entries) |
| Abbreviation 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 | (45 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 | (56 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
A [variable, in CoqEqDec]add [abbreviation, in MetatheoryAlt]
add [abbreviation, in Metatheory]
AltAsn [constructor, in AssumeList]
apply_tuple [definition, in CoqUniquenessTac]
app_eq_one [lemma, in AssumeList]
app_nil_2 [lemma, in AssumeList]
app_nil_1 [lemma, in AssumeList]
app_assoc [lemma, in AssumeList]
app_cons_not_nil [lemma, in CoqListFacts]
app_eq_cons [lemma, in CoqListFacts]
arrow [definition, in CoqUniquenessTac]
asn [inductive, in AssumeList]
AssocList [library]
AssortedListProperties [section, in AssumeList]
AssortedListProperties.l [variable, in AssumeList]
AssortedListProperties.l1 [variable, in AssumeList]
AssortedListProperties.l2 [variable, in AssumeList]
AssortedListProperties.l3 [variable, in AssumeList]
AssortedListProperties.x [variable, in AssumeList]
AssortedListProperties.X [variable, in AssumeList]
AssortedListProperties.y [variable, in AssumeList]
AssumeList [library]
ATOM [module, in MetatheoryAtom]
AtomDT [module, in MetatheoryAtom]
AtomDT.eq [definition, in MetatheoryAtom]
AtomDT.eq_dec [definition, in MetatheoryAtom]
AtomDT.eq_trans [definition, in MetatheoryAtom]
AtomDT.eq_sym [definition, in MetatheoryAtom]
AtomDT.eq_refl [definition, in MetatheoryAtom]
AtomDT.t [definition, in MetatheoryAtom]
AtomImpl [module, in MetatheoryAtom]
AtomImpl.atom [definition, in MetatheoryAtom]
AtomImpl.atom_fresh_for_list [lemma, in MetatheoryAtom]
AtomImpl.eq_atom_dec [definition, in MetatheoryAtom]
AtomImpl.max_lt_r [lemma, in MetatheoryAtom]
AtomImpl.nat_list_max [lemma, in MetatheoryAtom]
atoms [abbreviation, in MetatheoryAtom]
AtomSetDecide [module, in MetatheoryAtom]
AtomSetFacts [module, in MetatheoryAtom]
AtomSetImpl [module, in MetatheoryAtom]
AtomSetNotin [module, in MetatheoryAtom]
AtomSetProperties [module, in MetatheoryAtom]
atom_fresh [lemma, in MetatheoryAtom]
ATOM.atom [axiom, in MetatheoryAtom]
ATOM.atom_fresh_for_list [axiom, in MetatheoryAtom]
ATOM.eq_atom_dec [axiom, in MetatheoryAtom]
B
BasicDisjointFacts [section, in AssumeList]binds [definition, in AssumeList]
bindsAlt [definition, in AssumeList]
BindsDerived [section, in AssumeList]
BindsDerived.a [variable, in AssumeList]
BindsDerived.A [variable, in AssumeList]
BindsDerived.b [variable, in AssumeList]
BindsDerived.B [variable, in AssumeList]
BindsDerived.E [variable, in AssumeList]
BindsDerived.F [variable, in AssumeList]
BindsDerived.f1 [variable, in AssumeList]
BindsDerived.f2 [variable, in AssumeList]
BindsDerived.G [variable, in AssumeList]
BindsDerived.x [variable, in AssumeList]
BindsDerived.y [variable, in AssumeList]
BindsProperties [section, in AssumeList]
BindsProperties.a [variable, in AssumeList]
BindsProperties.A [variable, in AssumeList]
BindsProperties.b [variable, in AssumeList]
BindsProperties.B [variable, in AssumeList]
BindsProperties.E [variable, in AssumeList]
BindsProperties.F [variable, in AssumeList]
BindsProperties.G [variable, in AssumeList]
BindsProperties.x [variable, in AssumeList]
BindsProperties.y [variable, in AssumeList]
binds_map [abbreviation, in MetatheoryAlt]
binds_app_r [abbreviation, in MetatheoryAlt]
binds_app_l [abbreviation, in MetatheoryAlt]
binds_cons [abbreviation, in MetatheoryAlt]
binds_one [abbreviation, in MetatheoryAlt]
binds_map [abbreviation, in Metatheory]
binds_app_r [abbreviation, in Metatheory]
binds_app_l [abbreviation, in Metatheory]
binds_cons [abbreviation, in Metatheory]
binds_one [abbreviation, in Metatheory]
binds_In [lemma, in AssumeList]
binds_weaken [lemma, in AssumeList]
binds_map_2 [lemma, in AssumeList]
binds_app_uniq [lemma, in AssumeList]
binds_dom_contradiction [lemma, in AssumeList]
binds_app [lemma, in AssumeList]
binds_app_3 [lemma, in AssumeList]
binds_app_2 [lemma, in AssumeList]
binds_app_1 [lemma, in AssumeList]
binds_cons_iff [lemma, in AssumeList]
binds_cons_3 [lemma, in AssumeList]
binds_cons_2 [lemma, in AssumeList]
binds_cons_1 [lemma, in AssumeList]
binds_one_iff [lemma, in AssumeList]
binds_one_2 [lemma, in AssumeList]
binds_one_1 [lemma, in AssumeList]
binds_one_3 [lemma, in AssumeList]
binds_nil [lemma, in AssumeList]
C
cons_app_assoc [lemma, in AssumeList]cons_app_one [lemma, in AssumeList]
cons_eq_app [lemma, in CoqListFacts]
CoqEqDec [library]
CoqFSetDecide [library]
CoqFSetInterface [library]
CoqIntro [library]
CoqListFacts [library]
CoqUniquenessTac [library]
CoqUniquenessTacEx [library]
D
DecidableSorting [section, in CoqListFacts]DecidableSorting.A [variable, in CoqListFacts]
DecidableSorting.leA [variable, in CoqListFacts]
DecidableSorting.leA_dec [variable, in CoqListFacts]
Decide [module, in CoqFSetDecide]
Definitions [section, in AssumeList]
Definitions.A [variable, in AssumeList]
Definitions.B [variable, in AssumeList]
Definitions.C [variable, in AssumeList]
_ `notin` _ [notation, in AssumeList]
_ ~~ _ [notation, in AssumeList]
disjoint [definition, in AssumeList]
disjoint_map_r [lemma, in AssumeList]
disjoint_map_l [lemma, in AssumeList]
disjoint_map_2 [lemma, in AssumeList]
disjoint_map_1 [lemma, in AssumeList]
disjoint_app_r [lemma, in AssumeList]
disjoint_app_l [lemma, in AssumeList]
disjoint_app_3 [lemma, in AssumeList]
disjoint_app_2 [lemma, in AssumeList]
disjoint_app_1 [lemma, in AssumeList]
disjoint_one_r [lemma, in AssumeList]
disjoint_one_l [lemma, in AssumeList]
disjoint_one_2 [lemma, in AssumeList]
disjoint_one_1 [lemma, in AssumeList]
disjoint_sym [lemma, in AssumeList]
disjoint_sym_1 [lemma, in AssumeList]
dom [definition, in AssumeList]
dom_map [lemma, in AssumeList]
dom_app [lemma, in AssumeList]
dom_one [lemma, in AssumeList]
dom_consAlt [lemma, in AssumeList]
dom_consVar [lemma, in AssumeList]
dom_nil [lemma, in AssumeList]
E
elim_incl_app [lemma, in CoqListFacts]elim_incl_cons [lemma, in CoqListFacts]
elim_not_In_app [lemma, in CoqListFacts]
elim_not_In_cons [lemma, in CoqListFacts]
empty [abbreviation, in MetatheoryAlt]
empty [abbreviation, in Metatheory]
env [definition, in MetatheoryAlt]
EnvImpl [module, in Metatheory]
EqDec_eq_of_EqDec [instance, in CoqEqDec]
EqDec_eq [record, in CoqEqDec]
EqDec_eq [inductive, in CoqEqDec]
EqDec_atom [instance, in MetatheoryAtom]
eqlistA_unique [lemma, in CoqListFacts]
eqlistA_ind' [definition, in CoqListFacts]
eqlist_eq [lemma, in CoqListFacts]
Equal_union_compat [lemma, in LibLNgen]
equiv_decidable [lemma, in CoqEqDec]
equiv_transitive' [lemma, in CoqEqDec]
equiv_symmetric' [lemma, in CoqEqDec]
equiv_reflexive' [lemma, in CoqEqDec]
eq_var [abbreviation, in MetatheoryAlt]
eq_var [abbreviation, in Metatheory]
eq_dec [projection, in CoqEqDec]
eq_dec [constructor, in CoqEqDec]
eq_pair_dec [lemma, in CoqUniquenessTac]
eq_unit_dec [lemma, in CoqUniquenessTac]
erase [definition, in AssumeList]
example_pick_fresh_use [lemma, in MetatheoryAtom]
F
fresh_app_r [lemma, in AssumeList]fresh_app_l [lemma, in AssumeList]
fresh_mid_head [lemma, in AssumeList]
fresh_mid_tail [lemma, in AssumeList]
FSetExtra [library]
FSetWeakNotin [library]
Fsub_LetSum_Soundness [library]
Fsub_LetSum_Infrastructure [library]
Fsub_LetSum_Definitions [library]
Fsub_LetSum_Lemmas [library]
I
InA_iff_In [lemma, in CoqListFacts]InA_In [lemma, in CoqListFacts]
incl_nil [lemma, in CoqListFacts]
Inf [abbreviation, in CoqListFacts]
in_app [lemma, in AssumeList]
in_one [lemma, in AssumeList]
In_incl [lemma, in CoqListFacts]
In_map [lemma, in CoqListFacts]
L
lelistA_unique [lemma, in CoqListFacts]lelistA_ind' [definition, in CoqListFacts]
lelistA_dec [lemma, in CoqListFacts]
LibDefaultSimp [library]
LibLNgen [library]
LibTactics [library]
ListProperties [section, in AssumeList]
ListProperties.l [variable, in AssumeList]
ListProperties.l1 [variable, in AssumeList]
ListProperties.l2 [variable, in AssumeList]
ListProperties.l3 [variable, in AssumeList]
ListProperties.x [variable, in AssumeList]
ListProperties.X [variable, in AssumeList]
ListProperties.y [variable, in AssumeList]
list_rev [definition, in CoqUniquenessTac]
lt_ge_dec [definition, in LibLNgen]
M
Make [module, in FSetExtra]Make [module, in AssocList]
Make.alist_ind [lemma, in AssocList]
Make.app_eq_one [lemma, in AssocList]
Make.app_nil_2 [lemma, in AssocList]
Make.app_nil_1 [lemma, in AssocList]
Make.app_assoc [lemma, in AssocList]
Make.AssortedListProperties [section, in AssocList]
Make.AssortedListProperties.x [variable, in AssocList]
Make.AssortedListProperties.X [variable, in AssocList]
Make.AssortedListProperties.xs [variable, in AssocList]
Make.AssortedListProperties.ys [variable, in AssocList]
Make.AssortedListProperties.zs [variable, in AssocList]
Make.binds [definition, in AssocList]
Make.BindsDerived [section, in AssocList]
Make.BindsDerived.a [variable, in AssocList]
Make.BindsDerived.A [variable, in AssocList]
Make.BindsDerived.b [variable, in AssocList]
Make.BindsDerived.B [variable, in AssocList]
Make.BindsDerived.E [variable, in AssocList]
Make.BindsDerived.F [variable, in AssocList]
Make.BindsDerived.f [variable, in AssocList]
Make.BindsDerived.G [variable, in AssocList]
Make.BindsDerived.x [variable, in AssocList]
Make.BindsDerived.y [variable, in AssocList]
Make.BindsProperties [section, in AssocList]
Make.BindsProperties.a [variable, in AssocList]
Make.BindsProperties.A [variable, in AssocList]
Make.BindsProperties.b [variable, in AssocList]
Make.BindsProperties.B [variable, in AssocList]
Make.BindsProperties.E [variable, in AssocList]
Make.BindsProperties.F [variable, in AssocList]
Make.BindsProperties.f [variable, in AssocList]
Make.BindsProperties.G [variable, in AssocList]
Make.BindsProperties.x [variable, in AssocList]
Make.BindsProperties.y [variable, in AssocList]
Make.BindsProperties2 [section, in AssocList]
Make.BindsProperties2.a [variable, in AssocList]
Make.BindsProperties2.A [variable, in AssocList]
Make.BindsProperties2.b [variable, in AssocList]
Make.BindsProperties2.B [variable, in AssocList]
Make.BindsProperties2.E [variable, in AssocList]
Make.BindsProperties2.F [variable, in AssocList]
Make.BindsProperties2.f [variable, in AssocList]
Make.BindsProperties2.G [variable, in AssocList]
Make.BindsProperties2.x [variable, in AssocList]
Make.BindsProperties2.y [variable, in AssocList]
Make.binds_unique [lemma, in AssocList]
Make.binds_In_inv [lemma, in AssocList]
Make.binds_In [lemma, in AssocList]
Make.binds_remove_mid [lemma, in AssocList]
Make.binds_mid_eq [lemma, in AssocList]
Make.binds_weaken [lemma, in AssocList]
Make.binds_lookup_dec [lemma, in AssocList]
Make.binds_lookup [lemma, in AssocList]
Make.binds_dec [lemma, in AssocList]
Make.binds_cons_uniq_iff [lemma, in AssocList]
Make.binds_cons_uniq_1 [lemma, in AssocList]
Make.binds_app_uniq_iff [lemma, in AssocList]
Make.binds_app_uniq_1 [lemma, in AssocList]
Make.binds_dom_contradiction [lemma, in AssocList]
Make.binds_map_2 [lemma, in AssocList]
Make.binds_map_1 [lemma, in AssocList]
Make.binds_app_iff [lemma, in AssocList]
Make.binds_app_3 [lemma, in AssocList]
Make.binds_app_2 [lemma, in AssocList]
Make.binds_app_1 [lemma, in AssocList]
Make.binds_cons_iff [lemma, in AssocList]
Make.binds_cons_3 [lemma, in AssocList]
Make.binds_cons_2 [lemma, in AssocList]
Make.binds_cons_1 [lemma, in AssocList]
Make.binds_one_iff [lemma, in AssocList]
Make.binds_one_3 [lemma, in AssocList]
Make.binds_one_2 [lemma, in AssocList]
Make.binds_one_1 [lemma, in AssocList]
Make.binds_nil_iff [lemma, in AssocList]
Make.cons_app_assoc [lemma, in AssocList]
Make.cons_app_one [lemma, in AssocList]
Make.D [module, in AssocList]
Make.disjoint [definition, in FSetExtra]
Make.Disjoint [section, in AssocList]
Make.disjoint [definition, in AssocList]
Make.disjoint_map_r [lemma, in AssocList]
Make.disjoint_map_l [lemma, in AssocList]
Make.disjoint_map_2 [lemma, in AssocList]
Make.disjoint_map_1 [lemma, in AssocList]
Make.disjoint_app_r [lemma, in AssocList]
Make.disjoint_app_l [lemma, in AssocList]
Make.disjoint_app_3 [lemma, in AssocList]
Make.disjoint_app_2 [lemma, in AssocList]
Make.disjoint_app_1 [lemma, in AssocList]
Make.disjoint_cons_r [lemma, in AssocList]
Make.disjoint_cons_l [lemma, in AssocList]
Make.disjoint_cons_3 [lemma, in AssocList]
Make.disjoint_cons_2 [lemma, in AssocList]
Make.disjoint_cons_1 [lemma, in AssocList]
Make.disjoint_one_r [lemma, in AssocList]
Make.disjoint_one_l [lemma, in AssocList]
Make.disjoint_one_2 [lemma, in AssocList]
Make.disjoint_one_1 [lemma, in AssocList]
Make.disjoint_nil_1 [lemma, in AssocList]
Make.disjoint_sym [lemma, in AssocList]
Make.disjoint_sym_1 [lemma, in AssocList]
Make.dom [definition, in AssocList]
Make.dom_map [lemma, in AssocList]
Make.dom_app [lemma, in AssocList]
Make.dom_cons [lemma, in AssocList]
Make.dom_one [lemma, in AssocList]
Make.dom_nil [lemma, in AssocList]
Make.fresh_list [definition, in FSetExtra]
Make.fresh_app_r [lemma, in AssocList]
Make.fresh_app_l [lemma, in AssocList]
Make.fresh_mid_head [lemma, in AssocList]
Make.fresh_mid_tail [lemma, in AssocList]
Make.get [definition, in AssocList]
Make.in_app_iff [lemma, in AssocList]
Make.in_one_iff [lemma, in AssocList]
Make.in_nil_iff [lemma, in AssocList]
Make.KeySetFacts [module, in AssocList]
Make.KeySetProperties [module, in AssocList]
Make.ListProperties [section, in AssocList]
Make.ListProperties.l [variable, in AssocList]
Make.ListProperties.l1 [variable, in AssocList]
Make.ListProperties.l2 [variable, in AssocList]
Make.ListProperties.l3 [variable, in AssocList]
Make.ListProperties.x [variable, in AssocList]
Make.ListProperties.X [variable, in AssocList]
Make.ListProperties.y [variable, in AssocList]
Make.map [definition, in AssocList]
Make.maps [definition, in AssocList]
Make.map_app [lemma, in AssocList]
Make.map_cons [lemma, in AssocList]
Make.map_one [lemma, in AssocList]
Make.map_nil [lemma, in AssocList]
Make.nil_neq_one_mid [lemma, in AssocList]
Make.notin [definition, in FSetExtra]
Make.one [definition, in AssocList]
Make.one_mid_neq_nil [lemma, in AssocList]
Make.one_eq_app [lemma, in AssocList]
Make.Properties [section, in AssocList]
Make.Properties.A [variable, in AssocList]
Make.Properties.b [variable, in AssocList]
Make.Properties.B [variable, in AssocList]
Make.Properties.E [variable, in AssocList]
Make.Properties.F [variable, in AssocList]
Make.Properties.f [variable, in AssocList]
Make.Properties.G [variable, in AssocList]
Make.Properties.key [variable, in AssocList]
Make.Properties.x [variable, in AssocList]
Make.uniq [inductive, in AssocList]
Make.UniqDerived [section, in AssocList]
Make.UniqDerived.a [variable, in AssocList]
Make.UniqDerived.A [variable, in AssocList]
Make.UniqDerived.b [variable, in AssocList]
Make.UniqDerived.E [variable, in AssocList]
Make.UniqDerived.F [variable, in AssocList]
Make.UniqDerived.G [variable, in AssocList]
Make.UniqDerived.x [variable, in AssocList]
Make.UniqDerived.y [variable, in AssocList]
Make.UniqProperties [section, in AssocList]
Make.UniqProperties.a [variable, in AssocList]
Make.UniqProperties.A [variable, in AssocList]
Make.UniqProperties.b [variable, in AssocList]
Make.UniqProperties.B [variable, in AssocList]
Make.UniqProperties.E [variable, in AssocList]
Make.UniqProperties.F [variable, in AssocList]
Make.UniqProperties.f [variable, in AssocList]
Make.UniqProperties.G [variable, in AssocList]
Make.UniqProperties.x [variable, in AssocList]
Make.uniq_map_app_l [lemma, in AssocList]
Make.uniq_reorder_2 [lemma, in AssocList]
Make.uniq_reorder_1 [lemma, in AssocList]
Make.uniq_remove_mid [lemma, in AssocList]
Make.uniq_insert_mid [lemma, in AssocList]
Make.uniq_map_iff [lemma, in AssocList]
Make.uniq_map_2 [lemma, in AssocList]
Make.uniq_map_1 [lemma, in AssocList]
Make.uniq_app_iff [lemma, in AssocList]
Make.uniq_app_4 [lemma, in AssocList]
Make.uniq_app_3 [lemma, in AssocList]
Make.uniq_app_2 [lemma, in AssocList]
Make.uniq_app_1 [lemma, in AssocList]
Make.uniq_cons_iff [lemma, in AssocList]
Make.uniq_cons_3 [lemma, in AssocList]
Make.uniq_cons_2 [lemma, in AssocList]
Make.uniq_cons_1 [lemma, in AssocList]
Make.uniq_one_1 [lemma, in AssocList]
Make.uniq_push [constructor, in AssocList]
Make.uniq_nil [constructor, in AssocList]
_ ~ _ (list_scope) [notation, in AssocList]
map [definition, in AssumeList]
map_app [lemma, in AssumeList]
map_oneAlt [lemma, in AssumeList]
map_oneVar [lemma, in AssumeList]
map_consAlt [lemma, in AssumeList]
map_consVar [lemma, in AssumeList]
map_nil [lemma, in AssumeList]
Metatheory [library]
MetatheoryAlt [library]
MetatheoryAtom [library]
MoreBindsProperties [section, in AssumeList]
MoreBindsProperties.a [variable, in AssumeList]
MoreBindsProperties.A [variable, in AssumeList]
MoreBindsProperties.b [variable, in AssumeList]
MoreBindsProperties.B [variable, in AssumeList]
MoreBindsProperties.E [variable, in AssumeList]
MoreBindsProperties.F [variable, in AssumeList]
MoreBindsProperties.G [variable, in AssumeList]
MoreBindsProperties.x [variable, in AssumeList]
MoreBindsProperties.y [variable, in AssumeList]
N
nil_neq_one_mid [lemma, in AssumeList]nil_eq_app [lemma, in CoqListFacts]
notin_union [abbreviation, in MetatheoryAlt]
notin_singleton [abbreviation, in MetatheoryAlt]
notin_add [abbreviation, in MetatheoryAlt]
notin_empty [abbreviation, in MetatheoryAlt]
notin_union [abbreviation, in Metatheory]
notin_singleton [abbreviation, in Metatheory]
notin_add [abbreviation, in Metatheory]
notin_empty [abbreviation, in Metatheory]
Notin_fun.test_solve_notin_7 [lemma, in FSetWeakNotin]
Notin_fun.test_solve_notin_6 [lemma, in FSetWeakNotin]
Notin_fun.test_solve_notin_5 [lemma, in FSetWeakNotin]
Notin_fun.test_solve_notin_4 [lemma, in FSetWeakNotin]
Notin_fun.test_solve_notin_3 [lemma, in FSetWeakNotin]
Notin_fun.test_solve_notin_2 [lemma, in FSetWeakNotin]
Notin_fun.test_solve_notin_1 [lemma, in FSetWeakNotin]
Notin_fun.notin_diff_3 [lemma, in FSetWeakNotin]
Notin_fun.notin_diff_2 [lemma, in FSetWeakNotin]
Notin_fun.notin_diff_1 [lemma, in FSetWeakNotin]
Notin_fun.notin_inter_3 [lemma, in FSetWeakNotin]
Notin_fun.notin_inter_2 [lemma, in FSetWeakNotin]
Notin_fun.notin_inter_1 [lemma, in FSetWeakNotin]
Notin_fun.notin_union_3 [lemma, in FSetWeakNotin]
Notin_fun.notin_union_2 [lemma, in FSetWeakNotin]
Notin_fun.notin_union_1 [lemma, in FSetWeakNotin]
Notin_fun.notin_remove_3' [lemma, in FSetWeakNotin]
Notin_fun.notin_remove_3 [lemma, in FSetWeakNotin]
Notin_fun.notin_remove_2 [lemma, in FSetWeakNotin]
Notin_fun.notin_remove_1 [lemma, in FSetWeakNotin]
Notin_fun.notin_singleton_2 [lemma, in FSetWeakNotin]
Notin_fun.notin_singleton_1' [lemma, in FSetWeakNotin]
Notin_fun.notin_singleton_1 [lemma, in FSetWeakNotin]
Notin_fun.notin_add_3 [lemma, in FSetWeakNotin]
Notin_fun.notin_add_2 [lemma, in FSetWeakNotin]
Notin_fun.notin_add_1' [lemma, in FSetWeakNotin]
Notin_fun.notin_add_1 [lemma, in FSetWeakNotin]
Notin_fun.notin_empty_1 [lemma, in FSetWeakNotin]
Notin_fun.Lemmas.s' [variable, in FSetWeakNotin]
Notin_fun.Lemmas.s [variable, in FSetWeakNotin]
Notin_fun.Lemmas.y [variable, in FSetWeakNotin]
Notin_fun.Lemmas.x [variable, in FSetWeakNotin]
Notin_fun.Lemmas [section, in FSetWeakNotin]
Notin_fun.D [module, in FSetWeakNotin]
Notin_fun [module, in FSetWeakNotin]
not_In_app [lemma, in CoqListFacts]
not_In_cons [lemma, in CoqListFacts]
O
one [definition, in AssumeList]one_mid_neq_nil [lemma, in AssumeList]
one_eq_app [lemma, in AssumeList]
P
Properties [section, in AssumeList]Properties.a [variable, in AssumeList]
Properties.A [variable, in AssumeList]
Properties.b [variable, in AssumeList]
Properties.B [variable, in AssumeList]
Properties.E [variable, in AssumeList]
Properties.F [variable, in AssumeList]
Properties.f1 [variable, in AssumeList]
Properties.f2 [variable, in AssumeList]
Properties.G [variable, in AssumeList]
Properties.x [variable, in AssumeList]
R
remove [abbreviation, in MetatheoryAlt]remove [abbreviation, in Metatheory]
remove_union_distrib [lemma, in LibLNgen]
S
S [module, in CoqFSetInterface]Sdep [module, in CoqFSetInterface]
Sdep.add [axiom, in CoqFSetInterface]
Sdep.Add [definition, in CoqFSetInterface]
Sdep.cardinal [axiom, in CoqFSetInterface]
Sdep.choose [axiom, in CoqFSetInterface]
Sdep.choose_equal [axiom, in CoqFSetInterface]
Sdep.compare [axiom, in CoqFSetInterface]
Sdep.diff [axiom, in CoqFSetInterface]
Sdep.E [module, in CoqFSetInterface]
Sdep.elements [axiom, in CoqFSetInterface]
Sdep.elt [definition, in CoqFSetInterface]
Sdep.empty [axiom, in CoqFSetInterface]
Sdep.Empty [definition, in CoqFSetInterface]
Sdep.eq [definition, in CoqFSetInterface]
Sdep.equal [axiom, in CoqFSetInterface]
Sdep.Equal [definition, in CoqFSetInterface]
Sdep.eq_In [axiom, in CoqFSetInterface]
Sdep.eq_trans [axiom, in CoqFSetInterface]
Sdep.eq_sym [axiom, in CoqFSetInterface]
Sdep.eq_refl [axiom, in CoqFSetInterface]
Sdep.Exists [definition, in CoqFSetInterface]
Sdep.exists_ [axiom, in CoqFSetInterface]
Sdep.filter [axiom, in CoqFSetInterface]
Sdep.fold [axiom, in CoqFSetInterface]
Sdep.for_all [axiom, in CoqFSetInterface]
Sdep.For_all [definition, in CoqFSetInterface]
Sdep.In [axiom, in CoqFSetInterface]
Sdep.inter [axiom, in CoqFSetInterface]
Sdep.is_empty [axiom, in CoqFSetInterface]
Sdep.lt [axiom, in CoqFSetInterface]
Sdep.lt_not_eq [axiom, in CoqFSetInterface]
Sdep.lt_trans [axiom, in CoqFSetInterface]
Sdep.max_elt [axiom, in CoqFSetInterface]
Sdep.mem [axiom, in CoqFSetInterface]
Sdep.min_elt [axiom, in CoqFSetInterface]
Sdep.partition [axiom, in CoqFSetInterface]
Sdep.remove [axiom, in CoqFSetInterface]
Sdep.singleton [axiom, in CoqFSetInterface]
Sdep.subset [axiom, in CoqFSetInterface]
Sdep.Subset [definition, in CoqFSetInterface]
Sdep.t [axiom, in CoqFSetInterface]
Sdep.union [axiom, in CoqFSetInterface]
_ [=] _ [notation, in CoqFSetInterface]
Sfun [module, in CoqFSetInterface]
Sfun.choose_3 [axiom, in CoqFSetInterface]
Sfun.compare [axiom, in CoqFSetInterface]
Sfun.elements_3 [axiom, in CoqFSetInterface]
Sfun.lt [axiom, in CoqFSetInterface]
Sfun.lt_not_eq [axiom, in CoqFSetInterface]
Sfun.lt_trans [axiom, in CoqFSetInterface]
Sfun.max_elt_3 [axiom, in CoqFSetInterface]
Sfun.max_elt_2 [axiom, in CoqFSetInterface]
Sfun.max_elt_1 [axiom, in CoqFSetInterface]
Sfun.max_elt [axiom, in CoqFSetInterface]
Sfun.min_elt_3 [axiom, in CoqFSetInterface]
Sfun.min_elt_2 [axiom, in CoqFSetInterface]
Sfun.min_elt_1 [axiom, in CoqFSetInterface]
Sfun.min_elt [axiom, in CoqFSetInterface]
Sfun.Spec [section, in CoqFSetInterface]
Sfun.Spec.s [variable, in CoqFSetInterface]
Sfun.Spec.s' [variable, in CoqFSetInterface]
Sfun.Spec.s'' [variable, in CoqFSetInterface]
Sfun.Spec.x [variable, in CoqFSetInterface]
Sfun.Spec.y [variable, in CoqFSetInterface]
singleton [abbreviation, in MetatheoryAlt]
singleton [abbreviation, in Metatheory]
Sort [abbreviation, in CoqListFacts]
SortedListEquality [section, in CoqListFacts]
SortedListEquality.A [variable, in CoqListFacts]
SortedListEquality.eqA_ltA [variable, in CoqListFacts]
SortedListEquality.ltA [variable, in CoqListFacts]
SortedListEquality.ltA_eqA [variable, in CoqListFacts]
SortedListEquality.ltA_not_eqA [variable, in CoqListFacts]
SortedListEquality.ltA_trans [variable, in CoqListFacts]
sort_unique [lemma, in CoqListFacts]
sort_ind' [definition, in CoqListFacts]
Sort_In_eq [lemma, in CoqListFacts]
Sort_InA_eq [lemma, in CoqListFacts]
sort_dec [lemma, in CoqListFacts]
STLC [library]
STLCsol [library]
Subset_union_lngen_open_upper [lemma, in LibLNgen]
Subset_union_right [lemma, in LibLNgen]
Subset_union_left [lemma, in LibLNgen]
Subset_union_compat [lemma, in LibLNgen]
Subset_empty_any [lemma, in LibLNgen]
Subset_refl [lemma, in LibLNgen]
S.E [module, in CoqFSetInterface]
T
tr_tuple_rev [definition, in CoqUniquenessTac]tr_list_rev [definition, in CoqUniquenessTac]
tuple [definition, in CoqUniquenessTac]
tuple_rev [definition, in CoqUniquenessTac]
U
union [abbreviation, in MetatheoryAlt]union [abbreviation, in Metatheory]
union_map [definition, in Metatheory]
uniq [inductive, in AssumeList]
UniqDerived [section, in AssumeList]
UniqDerived.a [variable, in AssumeList]
UniqDerived.A [variable, in AssumeList]
UniqDerived.b [variable, in AssumeList]
UniqDerived.B [variable, in AssumeList]
UniqDerived.E [variable, in AssumeList]
UniqDerived.F [variable, in AssumeList]
UniqDerived.G [variable, in AssumeList]
UniqDerived.x [variable, in AssumeList]
UniqDerived.y [variable, in AssumeList]
UniqProperties [section, in AssumeList]
UniqProperties.A [variable, in AssumeList]
UniqProperties.b [variable, in AssumeList]
UniqProperties.B [variable, in AssumeList]
UniqProperties.E [variable, in AssumeList]
UniqProperties.F [variable, in AssumeList]
UniqProperties.f1 [variable, in AssumeList]
UniqProperties.f2 [variable, in AssumeList]
UniqProperties.G [variable, in AssumeList]
UniqProperties.x [variable, in AssumeList]
Uniqueness_Of_SetoidList_Proofs.list_eq_dec [variable, in CoqListFacts]
Uniqueness_Of_SetoidList_Proofs.R_unique [variable, in CoqListFacts]
Uniqueness_Of_SetoidList_Proofs.R [variable, in CoqListFacts]
Uniqueness_Of_SetoidList_Proofs.A [variable, in CoqListFacts]
Uniqueness_Of_SetoidList_Proofs [section, in CoqListFacts]
uniq_map [abbreviation, in MetatheoryAlt]
uniq_app [abbreviation, in MetatheoryAlt]
uniq_cons [abbreviation, in MetatheoryAlt]
uniq_one [abbreviation, in MetatheoryAlt]
uniq_map [abbreviation, in Metatheory]
uniq_app [abbreviation, in Metatheory]
uniq_cons [abbreviation, in Metatheory]
uniq_one [abbreviation, in Metatheory]
uniq_map_app_l [lemma, in AssumeList]
uniq_remove_mid [lemma, in AssumeList]
uniq_insert_mid [lemma, in AssumeList]
uniq_cons_3 [lemma, in AssumeList]
uniq_map [lemma, in AssumeList]
uniq_map_2 [lemma, in AssumeList]
uniq_map_1 [lemma, in AssumeList]
uniq_app [lemma, in AssumeList]
uniq_app_4 [lemma, in AssumeList]
uniq_app_3 [lemma, in AssumeList]
uniq_app_2 [lemma, in AssumeList]
uniq_app_1 [lemma, in AssumeList]
uniq_one_1 [lemma, in AssumeList]
uniq_alt [constructor, in AssumeList]
uniq_push [constructor, in AssumeList]
uniq_nil [constructor, in AssumeList]
V
var [abbreviation, in MetatheoryAlt]var [abbreviation, in Metatheory]
VarAsn [constructor, in AssumeList]
vars [abbreviation, in MetatheoryAlt]
vars [abbreviation, in Metatheory]
W
WDecide [module, in CoqFSetDecide]WDecide_fun.FSetDecideTestCases.test_baydemir_4 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_3 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_2 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.function_test_2 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.function_test_1 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_too_complex [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.eq_chain_test [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_set_ops_1 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_iff_conj [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_not_In_conj [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_not_In_disj [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_disjunction [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_Subset_add_remove [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_add_In [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_In_singleton [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_2 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_1 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_trans_2 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_trans_1 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases [module, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.dec_eq [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.dec_In [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.Equal_FSet_Prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.Subset_FSet_Prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.Empty_FSet_Prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.elt_FSet_Prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.FSet_Prop [inductive, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.not_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.impl_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.disj_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.conj_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.False_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.True_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.In_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.eq_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.eq_Prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.FSet_elt_Prop [inductive, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary [module, in CoqFSetDecide]
WDecide_fun.FSetLogicalFacts.test_pull [lemma, in CoqFSetDecide]
WDecide_fun.FSetLogicalFacts.test_push [lemma, in CoqFSetDecide]
WDecide_fun.FSetLogicalFacts [module, in CoqFSetDecide]
WDecide_fun.F [module, in CoqFSetDecide]
WDecide_fun [module, in CoqFSetDecide]
WS [module, in CoqFSetInterface]
WSfun [module, in CoqFSetInterface]
WSfun [module, in FSetExtra]
WSfun.add [axiom, in CoqFSetInterface]
WSfun.add_3 [axiom, in CoqFSetInterface]
WSfun.add_2 [axiom, in CoqFSetInterface]
WSfun.add_1 [axiom, in CoqFSetInterface]
WSfun.cardinal [axiom, in CoqFSetInterface]
WSfun.cardinal_1 [axiom, in CoqFSetInterface]
WSfun.choose [axiom, in CoqFSetInterface]
WSfun.choose_2 [axiom, in CoqFSetInterface]
WSfun.choose_1 [axiom, in CoqFSetInterface]
WSfun.diff [axiom, in CoqFSetInterface]
WSfun.diff_3 [axiom, in CoqFSetInterface]
WSfun.diff_2 [axiom, in CoqFSetInterface]
WSfun.diff_1 [axiom, in CoqFSetInterface]
WSfun.disjoint [definition, in FSetExtra]
WSfun.elements [axiom, in CoqFSetInterface]
WSfun.elements_3w [axiom, in CoqFSetInterface]
WSfun.elements_2 [axiom, in CoqFSetInterface]
WSfun.elements_1 [axiom, in CoqFSetInterface]
WSfun.elt [definition, in CoqFSetInterface]
WSfun.empty [axiom, in CoqFSetInterface]
WSfun.Empty [definition, in CoqFSetInterface]
WSfun.empty_1 [axiom, in CoqFSetInterface]
WSfun.eq [definition, in CoqFSetInterface]
WSfun.equal [axiom, in CoqFSetInterface]
WSfun.Equal [definition, in CoqFSetInterface]
WSfun.equal_2 [axiom, in CoqFSetInterface]
WSfun.equal_1 [axiom, in CoqFSetInterface]
WSfun.eq_trans [axiom, in CoqFSetInterface]
WSfun.eq_sym [axiom, in CoqFSetInterface]
WSfun.eq_refl [axiom, in CoqFSetInterface]
WSfun.eq_dec [axiom, in CoqFSetInterface]
WSfun.Exists [definition, in CoqFSetInterface]
WSfun.exists_2 [axiom, in CoqFSetInterface]
WSfun.exists_1 [axiom, in CoqFSetInterface]
WSfun.exists_ [axiom, in CoqFSetInterface]
WSfun.filter [axiom, in CoqFSetInterface]
WSfun.filter_3 [axiom, in CoqFSetInterface]
WSfun.filter_2 [axiom, in CoqFSetInterface]
WSfun.filter_1 [axiom, in CoqFSetInterface]
WSfun.fold [axiom, in CoqFSetInterface]
WSfun.fold_1 [axiom, in CoqFSetInterface]
WSfun.for_all_2 [axiom, in CoqFSetInterface]
WSfun.for_all_1 [axiom, in CoqFSetInterface]
WSfun.for_all [axiom, in CoqFSetInterface]
WSfun.For_all [definition, in CoqFSetInterface]
WSfun.fresh_list [definition, in FSetExtra]
WSfun.In [axiom, in CoqFSetInterface]
WSfun.inter [axiom, in CoqFSetInterface]
WSfun.inter_3 [axiom, in CoqFSetInterface]
WSfun.inter_2 [axiom, in CoqFSetInterface]
WSfun.inter_1 [axiom, in CoqFSetInterface]
WSfun.In_1 [axiom, in CoqFSetInterface]
WSfun.is_empty_2 [axiom, in CoqFSetInterface]
WSfun.is_empty_1 [axiom, in CoqFSetInterface]
WSfun.is_empty [axiom, in CoqFSetInterface]
WSfun.mem [axiom, in CoqFSetInterface]
WSfun.mem_2 [axiom, in CoqFSetInterface]
WSfun.mem_1 [axiom, in CoqFSetInterface]
WSfun.notin [definition, in FSetExtra]
WSfun.partition [axiom, in CoqFSetInterface]
WSfun.partition_2 [axiom, in CoqFSetInterface]
WSfun.partition_1 [axiom, in CoqFSetInterface]
WSfun.remove [axiom, in CoqFSetInterface]
WSfun.remove_3 [axiom, in CoqFSetInterface]
WSfun.remove_2 [axiom, in CoqFSetInterface]
WSfun.remove_1 [axiom, in CoqFSetInterface]
WSfun.singleton [axiom, in CoqFSetInterface]
WSfun.singleton_2 [axiom, in CoqFSetInterface]
WSfun.singleton_1 [axiom, in CoqFSetInterface]
WSfun.Spec [section, in CoqFSetInterface]
WSfun.Spec.Filter [section, in CoqFSetInterface]
WSfun.Spec.Filter.f [variable, in CoqFSetInterface]
WSfun.Spec.s [variable, in CoqFSetInterface]
WSfun.Spec.s' [variable, in CoqFSetInterface]
WSfun.Spec.s'' [variable, in CoqFSetInterface]
WSfun.Spec.x [variable, in CoqFSetInterface]
WSfun.Spec.y [variable, in CoqFSetInterface]
WSfun.subset [axiom, in CoqFSetInterface]
WSfun.Subset [definition, in CoqFSetInterface]
WSfun.subset_2 [axiom, in CoqFSetInterface]
WSfun.subset_1 [axiom, in CoqFSetInterface]
WSfun.t [axiom, in CoqFSetInterface]
WSfun.union [axiom, in CoqFSetInterface]
WSfun.union_3 [axiom, in CoqFSetInterface]
WSfun.union_2 [axiom, in CoqFSetInterface]
WSfun.union_1 [axiom, in CoqFSetInterface]
_ [<=] _ [notation, in CoqFSetInterface]
_ [=] _ [notation, in CoqFSetInterface]
WS.E [module, in CoqFSetInterface]
other
_ === _ (coqeqdec_scope) [notation, in MetatheoryAlt]_ == _ (coqeqdec_scope) [notation, in MetatheoryAlt]
_ === _ (coqeqdec_scope) [notation, in Metatheory]
_ == _ (coqeqdec_scope) [notation, in Metatheory]
[ _ ] (env_scope) [notation, in Metatheory]
_ \u _ (set_sl_scope) [notation, in MetatheoryAlt]
_ \notin _ (set_sl_scope) [notation, in MetatheoryAlt]
_ \in _ (set_sl_scope) [notation, in MetatheoryAlt]
_ `union` _ (set_hs_scope) [notation, in MetatheoryAlt]
_ `notin` _ (set_hs_scope) [notation, in MetatheoryAlt]
_ `in` _ (set_hs_scope) [notation, in MetatheoryAlt]
{{ _ }} (set_scope) [notation, in MetatheoryAlt]
{} (set_scope) [notation, in MetatheoryAlt]
_ [<=] _ (set_scope) [notation, in MetatheoryAlt]
_ [=] _ (set_scope) [notation, in MetatheoryAlt]
_ \u _ (set_sl_scope) [notation, in Metatheory]
_ \notin _ (set_sl_scope) [notation, in Metatheory]
_ \in _ (set_sl_scope) [notation, in Metatheory]
_ `union` _ (set_hs_scope) [notation, in Metatheory]
_ `notin` _ (set_hs_scope) [notation, in Metatheory]
_ `in` _ (set_hs_scope) [notation, in Metatheory]
{{ _ }} (set_scope) [notation, in Metatheory]
{} (set_scope) [notation, in Metatheory]
_ [<=] _ (set_scope) [notation, in Metatheory]
_ [=] _ (set_scope) [notation, in Metatheory]
_ [<=] _ [notation, in AssumeList]
_ [=] _ [notation, in AssumeList]
_ `notin` _ [notation, in AssumeList]
_ `in` _ [notation, in AssumeList]
_ `union` _ [notation, in AssumeList]
[ _ ] [notation, in AssumeList]
Notation Index
D
_ `notin` _ [in AssumeList]_ ~~ _ [in AssumeList]
M
_ ~ _ (list_scope) [in AssocList]S
_ [=] _ [in CoqFSetInterface]W
_ [<=] _ [in CoqFSetInterface]_ [=] _ [in CoqFSetInterface]
other
_ === _ (coqeqdec_scope) [in MetatheoryAlt]_ == _ (coqeqdec_scope) [in MetatheoryAlt]
_ === _ (coqeqdec_scope) [in Metatheory]
_ == _ (coqeqdec_scope) [in Metatheory]
[ _ ] (env_scope) [in Metatheory]
_ \u _ (set_sl_scope) [in MetatheoryAlt]
_ \notin _ (set_sl_scope) [in MetatheoryAlt]
_ \in _ (set_sl_scope) [in MetatheoryAlt]
_ `union` _ (set_hs_scope) [in MetatheoryAlt]
_ `notin` _ (set_hs_scope) [in MetatheoryAlt]
_ `in` _ (set_hs_scope) [in MetatheoryAlt]
{{ _ }} (set_scope) [in MetatheoryAlt]
{} (set_scope) [in MetatheoryAlt]
_ [<=] _ (set_scope) [in MetatheoryAlt]
_ [=] _ (set_scope) [in MetatheoryAlt]
_ \u _ (set_sl_scope) [in Metatheory]
_ \notin _ (set_sl_scope) [in Metatheory]
_ \in _ (set_sl_scope) [in Metatheory]
_ `union` _ (set_hs_scope) [in Metatheory]
_ `notin` _ (set_hs_scope) [in Metatheory]
_ `in` _ (set_hs_scope) [in Metatheory]
{{ _ }} (set_scope) [in Metatheory]
{} (set_scope) [in Metatheory]
_ [<=] _ (set_scope) [in Metatheory]
_ [=] _ (set_scope) [in Metatheory]
_ [<=] _ [in AssumeList]
_ [=] _ [in AssumeList]
_ `notin` _ [in AssumeList]
_ `in` _ [in AssumeList]
_ `union` _ [in AssumeList]
[ _ ] [in AssumeList]
Module Index
A
ATOM [in MetatheoryAtom]AtomDT [in MetatheoryAtom]
AtomImpl [in MetatheoryAtom]
AtomSetDecide [in MetatheoryAtom]
AtomSetFacts [in MetatheoryAtom]
AtomSetImpl [in MetatheoryAtom]
AtomSetNotin [in MetatheoryAtom]
AtomSetProperties [in MetatheoryAtom]
D
Decide [in CoqFSetDecide]E
EnvImpl [in Metatheory]M
Make [in FSetExtra]Make [in AssocList]
Make.D [in AssocList]
Make.KeySetFacts [in AssocList]
Make.KeySetProperties [in AssocList]
N
Notin_fun.D [in FSetWeakNotin]Notin_fun [in FSetWeakNotin]
S
S [in CoqFSetInterface]Sdep [in CoqFSetInterface]
Sdep.E [in CoqFSetInterface]
Sfun [in CoqFSetInterface]
S.E [in CoqFSetInterface]
W
WDecide [in CoqFSetDecide]WDecide_fun.FSetDecideTestCases [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary [in CoqFSetDecide]
WDecide_fun.FSetLogicalFacts [in CoqFSetDecide]
WDecide_fun.F [in CoqFSetDecide]
WDecide_fun [in CoqFSetDecide]
WS [in CoqFSetInterface]
WSfun [in CoqFSetInterface]
WSfun [in FSetExtra]
WS.E [in CoqFSetInterface]
Variable Index
A
A [in CoqEqDec]AssortedListProperties.l [in AssumeList]
AssortedListProperties.l1 [in AssumeList]
AssortedListProperties.l2 [in AssumeList]
AssortedListProperties.l3 [in AssumeList]
AssortedListProperties.x [in AssumeList]
AssortedListProperties.X [in AssumeList]
AssortedListProperties.y [in AssumeList]
B
BindsDerived.a [in AssumeList]BindsDerived.A [in AssumeList]
BindsDerived.b [in AssumeList]
BindsDerived.B [in AssumeList]
BindsDerived.E [in AssumeList]
BindsDerived.F [in AssumeList]
BindsDerived.f1 [in AssumeList]
BindsDerived.f2 [in AssumeList]
BindsDerived.G [in AssumeList]
BindsDerived.x [in AssumeList]
BindsDerived.y [in AssumeList]
BindsProperties.a [in AssumeList]
BindsProperties.A [in AssumeList]
BindsProperties.b [in AssumeList]
BindsProperties.B [in AssumeList]
BindsProperties.E [in AssumeList]
BindsProperties.F [in AssumeList]
BindsProperties.G [in AssumeList]
BindsProperties.x [in AssumeList]
BindsProperties.y [in AssumeList]
D
DecidableSorting.A [in CoqListFacts]DecidableSorting.leA [in CoqListFacts]
DecidableSorting.leA_dec [in CoqListFacts]
Definitions.A [in AssumeList]
Definitions.B [in AssumeList]
Definitions.C [in AssumeList]
L
ListProperties.l [in AssumeList]ListProperties.l1 [in AssumeList]
ListProperties.l2 [in AssumeList]
ListProperties.l3 [in AssumeList]
ListProperties.x [in AssumeList]
ListProperties.X [in AssumeList]
ListProperties.y [in AssumeList]
M
Make.AssortedListProperties.x [in AssocList]Make.AssortedListProperties.X [in AssocList]
Make.AssortedListProperties.xs [in AssocList]
Make.AssortedListProperties.ys [in AssocList]
Make.AssortedListProperties.zs [in AssocList]
Make.BindsDerived.a [in AssocList]
Make.BindsDerived.A [in AssocList]
Make.BindsDerived.b [in AssocList]
Make.BindsDerived.B [in AssocList]
Make.BindsDerived.E [in AssocList]
Make.BindsDerived.F [in AssocList]
Make.BindsDerived.f [in AssocList]
Make.BindsDerived.G [in AssocList]
Make.BindsDerived.x [in AssocList]
Make.BindsDerived.y [in AssocList]
Make.BindsProperties.a [in AssocList]
Make.BindsProperties.A [in AssocList]
Make.BindsProperties.b [in AssocList]
Make.BindsProperties.B [in AssocList]
Make.BindsProperties.E [in AssocList]
Make.BindsProperties.F [in AssocList]
Make.BindsProperties.f [in AssocList]
Make.BindsProperties.G [in AssocList]
Make.BindsProperties.x [in AssocList]
Make.BindsProperties.y [in AssocList]
Make.BindsProperties2.a [in AssocList]
Make.BindsProperties2.A [in AssocList]
Make.BindsProperties2.b [in AssocList]
Make.BindsProperties2.B [in AssocList]
Make.BindsProperties2.E [in AssocList]
Make.BindsProperties2.F [in AssocList]
Make.BindsProperties2.f [in AssocList]
Make.BindsProperties2.G [in AssocList]
Make.BindsProperties2.x [in AssocList]
Make.BindsProperties2.y [in AssocList]
Make.ListProperties.l [in AssocList]
Make.ListProperties.l1 [in AssocList]
Make.ListProperties.l2 [in AssocList]
Make.ListProperties.l3 [in AssocList]
Make.ListProperties.x [in AssocList]
Make.ListProperties.X [in AssocList]
Make.ListProperties.y [in AssocList]
Make.Properties.A [in AssocList]
Make.Properties.b [in AssocList]
Make.Properties.B [in AssocList]
Make.Properties.E [in AssocList]
Make.Properties.F [in AssocList]
Make.Properties.f [in AssocList]
Make.Properties.G [in AssocList]
Make.Properties.key [in AssocList]
Make.Properties.x [in AssocList]
Make.UniqDerived.a [in AssocList]
Make.UniqDerived.A [in AssocList]
Make.UniqDerived.b [in AssocList]
Make.UniqDerived.E [in AssocList]
Make.UniqDerived.F [in AssocList]
Make.UniqDerived.G [in AssocList]
Make.UniqDerived.x [in AssocList]
Make.UniqDerived.y [in AssocList]
Make.UniqProperties.a [in AssocList]
Make.UniqProperties.A [in AssocList]
Make.UniqProperties.b [in AssocList]
Make.UniqProperties.B [in AssocList]
Make.UniqProperties.E [in AssocList]
Make.UniqProperties.F [in AssocList]
Make.UniqProperties.f [in AssocList]
Make.UniqProperties.G [in AssocList]
Make.UniqProperties.x [in AssocList]
MoreBindsProperties.a [in AssumeList]
MoreBindsProperties.A [in AssumeList]
MoreBindsProperties.b [in AssumeList]
MoreBindsProperties.B [in AssumeList]
MoreBindsProperties.E [in AssumeList]
MoreBindsProperties.F [in AssumeList]
MoreBindsProperties.G [in AssumeList]
MoreBindsProperties.x [in AssumeList]
MoreBindsProperties.y [in AssumeList]
N
Notin_fun.Lemmas.s' [in FSetWeakNotin]Notin_fun.Lemmas.s [in FSetWeakNotin]
Notin_fun.Lemmas.y [in FSetWeakNotin]
Notin_fun.Lemmas.x [in FSetWeakNotin]
P
Properties.a [in AssumeList]Properties.A [in AssumeList]
Properties.b [in AssumeList]
Properties.B [in AssumeList]
Properties.E [in AssumeList]
Properties.F [in AssumeList]
Properties.f1 [in AssumeList]
Properties.f2 [in AssumeList]
Properties.G [in AssumeList]
Properties.x [in AssumeList]
S
Sfun.Spec.s [in CoqFSetInterface]Sfun.Spec.s' [in CoqFSetInterface]
Sfun.Spec.s'' [in CoqFSetInterface]
Sfun.Spec.x [in CoqFSetInterface]
Sfun.Spec.y [in CoqFSetInterface]
SortedListEquality.A [in CoqListFacts]
SortedListEquality.eqA_ltA [in CoqListFacts]
SortedListEquality.ltA [in CoqListFacts]
SortedListEquality.ltA_eqA [in CoqListFacts]
SortedListEquality.ltA_not_eqA [in CoqListFacts]
SortedListEquality.ltA_trans [in CoqListFacts]
U
UniqDerived.a [in AssumeList]UniqDerived.A [in AssumeList]
UniqDerived.b [in AssumeList]
UniqDerived.B [in AssumeList]
UniqDerived.E [in AssumeList]
UniqDerived.F [in AssumeList]
UniqDerived.G [in AssumeList]
UniqDerived.x [in AssumeList]
UniqDerived.y [in AssumeList]
UniqProperties.A [in AssumeList]
UniqProperties.b [in AssumeList]
UniqProperties.B [in AssumeList]
UniqProperties.E [in AssumeList]
UniqProperties.F [in AssumeList]
UniqProperties.f1 [in AssumeList]
UniqProperties.f2 [in AssumeList]
UniqProperties.G [in AssumeList]
UniqProperties.x [in AssumeList]
Uniqueness_Of_SetoidList_Proofs.list_eq_dec [in CoqListFacts]
Uniqueness_Of_SetoidList_Proofs.R_unique [in CoqListFacts]
Uniqueness_Of_SetoidList_Proofs.R [in CoqListFacts]
Uniqueness_Of_SetoidList_Proofs.A [in CoqListFacts]
W
WSfun.Spec.Filter.f [in CoqFSetInterface]WSfun.Spec.s [in CoqFSetInterface]
WSfun.Spec.s' [in CoqFSetInterface]
WSfun.Spec.s'' [in CoqFSetInterface]
WSfun.Spec.x [in CoqFSetInterface]
WSfun.Spec.y [in CoqFSetInterface]
Library Index
A
AssocListAssumeList
C
CoqEqDecCoqFSetDecide
CoqFSetInterface
CoqIntro
CoqListFacts
CoqUniquenessTac
CoqUniquenessTacEx
F
FSetExtraFSetWeakNotin
Fsub_LetSum_Soundness
Fsub_LetSum_Infrastructure
Fsub_LetSum_Definitions
Fsub_LetSum_Lemmas
L
LibDefaultSimpLibLNgen
LibTactics
M
MetatheoryMetatheoryAlt
MetatheoryAtom
S
STLCSTLCsol
Axiom Index
A
ATOM.atom [in MetatheoryAtom]ATOM.atom_fresh_for_list [in MetatheoryAtom]
ATOM.eq_atom_dec [in MetatheoryAtom]
S
Sdep.add [in CoqFSetInterface]Sdep.cardinal [in CoqFSetInterface]
Sdep.choose [in CoqFSetInterface]
Sdep.choose_equal [in CoqFSetInterface]
Sdep.compare [in CoqFSetInterface]
Sdep.diff [in CoqFSetInterface]
Sdep.elements [in CoqFSetInterface]
Sdep.empty [in CoqFSetInterface]
Sdep.equal [in CoqFSetInterface]
Sdep.eq_In [in CoqFSetInterface]
Sdep.eq_trans [in CoqFSetInterface]
Sdep.eq_sym [in CoqFSetInterface]
Sdep.eq_refl [in CoqFSetInterface]
Sdep.exists_ [in CoqFSetInterface]
Sdep.filter [in CoqFSetInterface]
Sdep.fold [in CoqFSetInterface]
Sdep.for_all [in CoqFSetInterface]
Sdep.In [in CoqFSetInterface]
Sdep.inter [in CoqFSetInterface]
Sdep.is_empty [in CoqFSetInterface]
Sdep.lt [in CoqFSetInterface]
Sdep.lt_not_eq [in CoqFSetInterface]
Sdep.lt_trans [in CoqFSetInterface]
Sdep.max_elt [in CoqFSetInterface]
Sdep.mem [in CoqFSetInterface]
Sdep.min_elt [in CoqFSetInterface]
Sdep.partition [in CoqFSetInterface]
Sdep.remove [in CoqFSetInterface]
Sdep.singleton [in CoqFSetInterface]
Sdep.subset [in CoqFSetInterface]
Sdep.t [in CoqFSetInterface]
Sdep.union [in CoqFSetInterface]
Sfun.choose_3 [in CoqFSetInterface]
Sfun.compare [in CoqFSetInterface]
Sfun.elements_3 [in CoqFSetInterface]
Sfun.lt [in CoqFSetInterface]
Sfun.lt_not_eq [in CoqFSetInterface]
Sfun.lt_trans [in CoqFSetInterface]
Sfun.max_elt_3 [in CoqFSetInterface]
Sfun.max_elt_2 [in CoqFSetInterface]
Sfun.max_elt_1 [in CoqFSetInterface]
Sfun.max_elt [in CoqFSetInterface]
Sfun.min_elt_3 [in CoqFSetInterface]
Sfun.min_elt_2 [in CoqFSetInterface]
Sfun.min_elt_1 [in CoqFSetInterface]
Sfun.min_elt [in CoqFSetInterface]
W
WSfun.add [in CoqFSetInterface]WSfun.add_3 [in CoqFSetInterface]
WSfun.add_2 [in CoqFSetInterface]
WSfun.add_1 [in CoqFSetInterface]
WSfun.cardinal [in CoqFSetInterface]
WSfun.cardinal_1 [in CoqFSetInterface]
WSfun.choose [in CoqFSetInterface]
WSfun.choose_2 [in CoqFSetInterface]
WSfun.choose_1 [in CoqFSetInterface]
WSfun.diff [in CoqFSetInterface]
WSfun.diff_3 [in CoqFSetInterface]
WSfun.diff_2 [in CoqFSetInterface]
WSfun.diff_1 [in CoqFSetInterface]
WSfun.elements [in CoqFSetInterface]
WSfun.elements_3w [in CoqFSetInterface]
WSfun.elements_2 [in CoqFSetInterface]
WSfun.elements_1 [in CoqFSetInterface]
WSfun.empty [in CoqFSetInterface]
WSfun.empty_1 [in CoqFSetInterface]
WSfun.equal [in CoqFSetInterface]
WSfun.equal_2 [in CoqFSetInterface]
WSfun.equal_1 [in CoqFSetInterface]
WSfun.eq_trans [in CoqFSetInterface]
WSfun.eq_sym [in CoqFSetInterface]
WSfun.eq_refl [in CoqFSetInterface]
WSfun.eq_dec [in CoqFSetInterface]
WSfun.exists_2 [in CoqFSetInterface]
WSfun.exists_1 [in CoqFSetInterface]
WSfun.exists_ [in CoqFSetInterface]
WSfun.filter [in CoqFSetInterface]
WSfun.filter_3 [in CoqFSetInterface]
WSfun.filter_2 [in CoqFSetInterface]
WSfun.filter_1 [in CoqFSetInterface]
WSfun.fold [in CoqFSetInterface]
WSfun.fold_1 [in CoqFSetInterface]
WSfun.for_all_2 [in CoqFSetInterface]
WSfun.for_all_1 [in CoqFSetInterface]
WSfun.for_all [in CoqFSetInterface]
WSfun.In [in CoqFSetInterface]
WSfun.inter [in CoqFSetInterface]
WSfun.inter_3 [in CoqFSetInterface]
WSfun.inter_2 [in CoqFSetInterface]
WSfun.inter_1 [in CoqFSetInterface]
WSfun.In_1 [in CoqFSetInterface]
WSfun.is_empty_2 [in CoqFSetInterface]
WSfun.is_empty_1 [in CoqFSetInterface]
WSfun.is_empty [in CoqFSetInterface]
WSfun.mem [in CoqFSetInterface]
WSfun.mem_2 [in CoqFSetInterface]
WSfun.mem_1 [in CoqFSetInterface]
WSfun.partition [in CoqFSetInterface]
WSfun.partition_2 [in CoqFSetInterface]
WSfun.partition_1 [in CoqFSetInterface]
WSfun.remove [in CoqFSetInterface]
WSfun.remove_3 [in CoqFSetInterface]
WSfun.remove_2 [in CoqFSetInterface]
WSfun.remove_1 [in CoqFSetInterface]
WSfun.singleton [in CoqFSetInterface]
WSfun.singleton_2 [in CoqFSetInterface]
WSfun.singleton_1 [in CoqFSetInterface]
WSfun.subset [in CoqFSetInterface]
WSfun.subset_2 [in CoqFSetInterface]
WSfun.subset_1 [in CoqFSetInterface]
WSfun.t [in CoqFSetInterface]
WSfun.union [in CoqFSetInterface]
WSfun.union_3 [in CoqFSetInterface]
WSfun.union_2 [in CoqFSetInterface]
WSfun.union_1 [in CoqFSetInterface]
Constructor Index
A
AltAsn [in AssumeList]E
eq_dec [in CoqEqDec]M
Make.uniq_push [in AssocList]Make.uniq_nil [in AssocList]
U
uniq_alt [in AssumeList]uniq_push [in AssumeList]
uniq_nil [in AssumeList]
V
VarAsn [in AssumeList]W
WDecide_fun.FSetDecideAuxiliary.Equal_FSet_Prop [in CoqFSetDecide]WDecide_fun.FSetDecideAuxiliary.Subset_FSet_Prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.Empty_FSet_Prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.elt_FSet_Prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.not_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.impl_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.disj_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.conj_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.False_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.True_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.In_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.eq_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.eq_Prop [in CoqFSetDecide]
Lemma Index
A
app_eq_one [in AssumeList]app_nil_2 [in AssumeList]
app_nil_1 [in AssumeList]
app_assoc [in AssumeList]
app_cons_not_nil [in CoqListFacts]
app_eq_cons [in CoqListFacts]
AtomImpl.atom_fresh_for_list [in MetatheoryAtom]
AtomImpl.max_lt_r [in MetatheoryAtom]
AtomImpl.nat_list_max [in MetatheoryAtom]
atom_fresh [in MetatheoryAtom]
B
binds_In [in AssumeList]binds_weaken [in AssumeList]
binds_map_2 [in AssumeList]
binds_app_uniq [in AssumeList]
binds_dom_contradiction [in AssumeList]
binds_app [in AssumeList]
binds_app_3 [in AssumeList]
binds_app_2 [in AssumeList]
binds_app_1 [in AssumeList]
binds_cons_iff [in AssumeList]
binds_cons_3 [in AssumeList]
binds_cons_2 [in AssumeList]
binds_cons_1 [in AssumeList]
binds_one_iff [in AssumeList]
binds_one_2 [in AssumeList]
binds_one_1 [in AssumeList]
binds_one_3 [in AssumeList]
binds_nil [in AssumeList]
C
cons_app_assoc [in AssumeList]cons_app_one [in AssumeList]
cons_eq_app [in CoqListFacts]
D
disjoint_map_r [in AssumeList]disjoint_map_l [in AssumeList]
disjoint_map_2 [in AssumeList]
disjoint_map_1 [in AssumeList]
disjoint_app_r [in AssumeList]
disjoint_app_l [in AssumeList]
disjoint_app_3 [in AssumeList]
disjoint_app_2 [in AssumeList]
disjoint_app_1 [in AssumeList]
disjoint_one_r [in AssumeList]
disjoint_one_l [in AssumeList]
disjoint_one_2 [in AssumeList]
disjoint_one_1 [in AssumeList]
disjoint_sym [in AssumeList]
disjoint_sym_1 [in AssumeList]
dom_map [in AssumeList]
dom_app [in AssumeList]
dom_one [in AssumeList]
dom_consAlt [in AssumeList]
dom_consVar [in AssumeList]
dom_nil [in AssumeList]
E
elim_incl_app [in CoqListFacts]elim_incl_cons [in CoqListFacts]
elim_not_In_app [in CoqListFacts]
elim_not_In_cons [in CoqListFacts]
eqlistA_unique [in CoqListFacts]
eqlist_eq [in CoqListFacts]
Equal_union_compat [in LibLNgen]
equiv_decidable [in CoqEqDec]
equiv_transitive' [in CoqEqDec]
equiv_symmetric' [in CoqEqDec]
equiv_reflexive' [in CoqEqDec]
eq_pair_dec [in CoqUniquenessTac]
eq_unit_dec [in CoqUniquenessTac]
example_pick_fresh_use [in MetatheoryAtom]
F
fresh_app_r [in AssumeList]fresh_app_l [in AssumeList]
fresh_mid_head [in AssumeList]
fresh_mid_tail [in AssumeList]
I
InA_iff_In [in CoqListFacts]InA_In [in CoqListFacts]
incl_nil [in CoqListFacts]
in_app [in AssumeList]
in_one [in AssumeList]
In_incl [in CoqListFacts]
In_map [in CoqListFacts]
L
lelistA_unique [in CoqListFacts]lelistA_dec [in CoqListFacts]
M
Make.alist_ind [in AssocList]Make.app_eq_one [in AssocList]
Make.app_nil_2 [in AssocList]
Make.app_nil_1 [in AssocList]
Make.app_assoc [in AssocList]
Make.binds_unique [in AssocList]
Make.binds_In_inv [in AssocList]
Make.binds_In [in AssocList]
Make.binds_remove_mid [in AssocList]
Make.binds_mid_eq [in AssocList]
Make.binds_weaken [in AssocList]
Make.binds_lookup_dec [in AssocList]
Make.binds_lookup [in AssocList]
Make.binds_dec [in AssocList]
Make.binds_cons_uniq_iff [in AssocList]
Make.binds_cons_uniq_1 [in AssocList]
Make.binds_app_uniq_iff [in AssocList]
Make.binds_app_uniq_1 [in AssocList]
Make.binds_dom_contradiction [in AssocList]
Make.binds_map_2 [in AssocList]
Make.binds_map_1 [in AssocList]
Make.binds_app_iff [in AssocList]
Make.binds_app_3 [in AssocList]
Make.binds_app_2 [in AssocList]
Make.binds_app_1 [in AssocList]
Make.binds_cons_iff [in AssocList]
Make.binds_cons_3 [in AssocList]
Make.binds_cons_2 [in AssocList]
Make.binds_cons_1 [in AssocList]
Make.binds_one_iff [in AssocList]
Make.binds_one_3 [in AssocList]
Make.binds_one_2 [in AssocList]
Make.binds_one_1 [in AssocList]
Make.binds_nil_iff [in AssocList]
Make.cons_app_assoc [in AssocList]
Make.cons_app_one [in AssocList]
Make.disjoint_map_r [in AssocList]
Make.disjoint_map_l [in AssocList]
Make.disjoint_map_2 [in AssocList]
Make.disjoint_map_1 [in AssocList]
Make.disjoint_app_r [in AssocList]
Make.disjoint_app_l [in AssocList]
Make.disjoint_app_3 [in AssocList]
Make.disjoint_app_2 [in AssocList]
Make.disjoint_app_1 [in AssocList]
Make.disjoint_cons_r [in AssocList]
Make.disjoint_cons_l [in AssocList]
Make.disjoint_cons_3 [in AssocList]
Make.disjoint_cons_2 [in AssocList]
Make.disjoint_cons_1 [in AssocList]
Make.disjoint_one_r [in AssocList]
Make.disjoint_one_l [in AssocList]
Make.disjoint_one_2 [in AssocList]
Make.disjoint_one_1 [in AssocList]
Make.disjoint_nil_1 [in AssocList]
Make.disjoint_sym [in AssocList]
Make.disjoint_sym_1 [in AssocList]
Make.dom_map [in AssocList]
Make.dom_app [in AssocList]
Make.dom_cons [in AssocList]
Make.dom_one [in AssocList]
Make.dom_nil [in AssocList]
Make.fresh_app_r [in AssocList]
Make.fresh_app_l [in AssocList]
Make.fresh_mid_head [in AssocList]
Make.fresh_mid_tail [in AssocList]
Make.in_app_iff [in AssocList]
Make.in_one_iff [in AssocList]
Make.in_nil_iff [in AssocList]
Make.map_app [in AssocList]
Make.map_cons [in AssocList]
Make.map_one [in AssocList]
Make.map_nil [in AssocList]
Make.nil_neq_one_mid [in AssocList]
Make.one_mid_neq_nil [in AssocList]
Make.one_eq_app [in AssocList]
Make.uniq_map_app_l [in AssocList]
Make.uniq_reorder_2 [in AssocList]
Make.uniq_reorder_1 [in AssocList]
Make.uniq_remove_mid [in AssocList]
Make.uniq_insert_mid [in AssocList]
Make.uniq_map_iff [in AssocList]
Make.uniq_map_2 [in AssocList]
Make.uniq_map_1 [in AssocList]
Make.uniq_app_iff [in AssocList]
Make.uniq_app_4 [in AssocList]
Make.uniq_app_3 [in AssocList]
Make.uniq_app_2 [in AssocList]
Make.uniq_app_1 [in AssocList]
Make.uniq_cons_iff [in AssocList]
Make.uniq_cons_3 [in AssocList]
Make.uniq_cons_2 [in AssocList]
Make.uniq_cons_1 [in AssocList]
Make.uniq_one_1 [in AssocList]
map_app [in AssumeList]
map_oneAlt [in AssumeList]
map_oneVar [in AssumeList]
map_consAlt [in AssumeList]
map_consVar [in AssumeList]
map_nil [in AssumeList]
N
nil_neq_one_mid [in AssumeList]nil_eq_app [in CoqListFacts]
Notin_fun.test_solve_notin_7 [in FSetWeakNotin]
Notin_fun.test_solve_notin_6 [in FSetWeakNotin]
Notin_fun.test_solve_notin_5 [in FSetWeakNotin]
Notin_fun.test_solve_notin_4 [in FSetWeakNotin]
Notin_fun.test_solve_notin_3 [in FSetWeakNotin]
Notin_fun.test_solve_notin_2 [in FSetWeakNotin]
Notin_fun.test_solve_notin_1 [in FSetWeakNotin]
Notin_fun.notin_diff_3 [in FSetWeakNotin]
Notin_fun.notin_diff_2 [in FSetWeakNotin]
Notin_fun.notin_diff_1 [in FSetWeakNotin]
Notin_fun.notin_inter_3 [in FSetWeakNotin]
Notin_fun.notin_inter_2 [in FSetWeakNotin]
Notin_fun.notin_inter_1 [in FSetWeakNotin]
Notin_fun.notin_union_3 [in FSetWeakNotin]
Notin_fun.notin_union_2 [in FSetWeakNotin]
Notin_fun.notin_union_1 [in FSetWeakNotin]
Notin_fun.notin_remove_3' [in FSetWeakNotin]
Notin_fun.notin_remove_3 [in FSetWeakNotin]
Notin_fun.notin_remove_2 [in FSetWeakNotin]
Notin_fun.notin_remove_1 [in FSetWeakNotin]
Notin_fun.notin_singleton_2 [in FSetWeakNotin]
Notin_fun.notin_singleton_1' [in FSetWeakNotin]
Notin_fun.notin_singleton_1 [in FSetWeakNotin]
Notin_fun.notin_add_3 [in FSetWeakNotin]
Notin_fun.notin_add_2 [in FSetWeakNotin]
Notin_fun.notin_add_1' [in FSetWeakNotin]
Notin_fun.notin_add_1 [in FSetWeakNotin]
Notin_fun.notin_empty_1 [in FSetWeakNotin]
not_In_app [in CoqListFacts]
not_In_cons [in CoqListFacts]
O
one_mid_neq_nil [in AssumeList]one_eq_app [in AssumeList]
R
remove_union_distrib [in LibLNgen]S
sort_unique [in CoqListFacts]Sort_In_eq [in CoqListFacts]
Sort_InA_eq [in CoqListFacts]
sort_dec [in CoqListFacts]
Subset_union_lngen_open_upper [in LibLNgen]
Subset_union_right [in LibLNgen]
Subset_union_left [in LibLNgen]
Subset_union_compat [in LibLNgen]
Subset_empty_any [in LibLNgen]
Subset_refl [in LibLNgen]
U
uniq_map_app_l [in AssumeList]uniq_remove_mid [in AssumeList]
uniq_insert_mid [in AssumeList]
uniq_cons_3 [in AssumeList]
uniq_map [in AssumeList]
uniq_map_2 [in AssumeList]
uniq_map_1 [in AssumeList]
uniq_app [in AssumeList]
uniq_app_4 [in AssumeList]
uniq_app_3 [in AssumeList]
uniq_app_2 [in AssumeList]
uniq_app_1 [in AssumeList]
uniq_one_1 [in AssumeList]
W
WDecide_fun.FSetDecideTestCases.test_baydemir_4 [in CoqFSetDecide]WDecide_fun.FSetDecideTestCases.test_baydemir_3 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_2 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.function_test_2 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.function_test_1 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_too_complex [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.eq_chain_test [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_set_ops_1 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_iff_conj [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_not_In_conj [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_not_In_disj [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_disjunction [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_Subset_add_remove [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_add_In [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_In_singleton [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_2 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_1 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_trans_2 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_trans_1 [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.dec_eq [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.dec_In [in CoqFSetDecide]
WDecide_fun.FSetLogicalFacts.test_pull [in CoqFSetDecide]
WDecide_fun.FSetLogicalFacts.test_push [in CoqFSetDecide]
Projection Index
E
eq_dec [in CoqEqDec]Inductive Index
A
asn [in AssumeList]E
EqDec_eq [in CoqEqDec]M
Make.uniq [in AssocList]U
uniq [in AssumeList]W
WDecide_fun.FSetDecideAuxiliary.FSet_Prop [in CoqFSetDecide]WDecide_fun.FSetDecideAuxiliary.FSet_elt_Prop [in CoqFSetDecide]
Section Index
A
AssortedListProperties [in AssumeList]B
BasicDisjointFacts [in AssumeList]BindsDerived [in AssumeList]
BindsProperties [in AssumeList]
D
DecidableSorting [in CoqListFacts]Definitions [in AssumeList]
L
ListProperties [in AssumeList]M
Make.AssortedListProperties [in AssocList]Make.BindsDerived [in AssocList]
Make.BindsProperties [in AssocList]
Make.BindsProperties2 [in AssocList]
Make.Disjoint [in AssocList]
Make.ListProperties [in AssocList]
Make.Properties [in AssocList]
Make.UniqDerived [in AssocList]
Make.UniqProperties [in AssocList]
MoreBindsProperties [in AssumeList]
N
Notin_fun.Lemmas [in FSetWeakNotin]P
Properties [in AssumeList]S
Sfun.Spec [in CoqFSetInterface]SortedListEquality [in CoqListFacts]
U
UniqDerived [in AssumeList]UniqProperties [in AssumeList]
Uniqueness_Of_SetoidList_Proofs [in CoqListFacts]
W
WSfun.Spec [in CoqFSetInterface]WSfun.Spec.Filter [in CoqFSetInterface]
Instance Index
E
EqDec_eq_of_EqDec [in CoqEqDec]EqDec_atom [in MetatheoryAtom]
Abbreviation Index
A
add [in MetatheoryAlt]add [in Metatheory]
atoms [in MetatheoryAtom]
B
binds_map [in MetatheoryAlt]binds_app_r [in MetatheoryAlt]
binds_app_l [in MetatheoryAlt]
binds_cons [in MetatheoryAlt]
binds_one [in MetatheoryAlt]
binds_map [in Metatheory]
binds_app_r [in Metatheory]
binds_app_l [in Metatheory]
binds_cons [in Metatheory]
binds_one [in Metatheory]
E
empty [in MetatheoryAlt]empty [in Metatheory]
eq_var [in MetatheoryAlt]
eq_var [in Metatheory]
I
Inf [in CoqListFacts]N
notin_union [in MetatheoryAlt]notin_singleton [in MetatheoryAlt]
notin_add [in MetatheoryAlt]
notin_empty [in MetatheoryAlt]
notin_union [in Metatheory]
notin_singleton [in Metatheory]
notin_add [in Metatheory]
notin_empty [in Metatheory]
R
remove [in MetatheoryAlt]remove [in Metatheory]
S
singleton [in MetatheoryAlt]singleton [in Metatheory]
Sort [in CoqListFacts]
U
union [in MetatheoryAlt]union [in Metatheory]
uniq_map [in MetatheoryAlt]
uniq_app [in MetatheoryAlt]
uniq_cons [in MetatheoryAlt]
uniq_one [in MetatheoryAlt]
uniq_map [in Metatheory]
uniq_app [in Metatheory]
uniq_cons [in Metatheory]
uniq_one [in Metatheory]
V
var [in MetatheoryAlt]var [in Metatheory]
vars [in MetatheoryAlt]
vars [in Metatheory]
Definition Index
A
apply_tuple [in CoqUniquenessTac]arrow [in CoqUniquenessTac]
AtomDT.eq [in MetatheoryAtom]
AtomDT.eq_dec [in MetatheoryAtom]
AtomDT.eq_trans [in MetatheoryAtom]
AtomDT.eq_sym [in MetatheoryAtom]
AtomDT.eq_refl [in MetatheoryAtom]
AtomDT.t [in MetatheoryAtom]
AtomImpl.atom [in MetatheoryAtom]
AtomImpl.eq_atom_dec [in MetatheoryAtom]
B
binds [in AssumeList]bindsAlt [in AssumeList]
D
disjoint [in AssumeList]dom [in AssumeList]
E
env [in MetatheoryAlt]eqlistA_ind' [in CoqListFacts]
erase [in AssumeList]
L
lelistA_ind' [in CoqListFacts]list_rev [in CoqUniquenessTac]
lt_ge_dec [in LibLNgen]
M
Make.binds [in AssocList]Make.disjoint [in FSetExtra]
Make.disjoint [in AssocList]
Make.dom [in AssocList]
Make.fresh_list [in FSetExtra]
Make.get [in AssocList]
Make.map [in AssocList]
Make.maps [in AssocList]
Make.notin [in FSetExtra]
Make.one [in AssocList]
map [in AssumeList]
O
one [in AssumeList]S
Sdep.Add [in CoqFSetInterface]Sdep.elt [in CoqFSetInterface]
Sdep.Empty [in CoqFSetInterface]
Sdep.eq [in CoqFSetInterface]
Sdep.Equal [in CoqFSetInterface]
Sdep.Exists [in CoqFSetInterface]
Sdep.For_all [in CoqFSetInterface]
Sdep.Subset [in CoqFSetInterface]
sort_ind' [in CoqListFacts]
T
tr_tuple_rev [in CoqUniquenessTac]tr_list_rev [in CoqUniquenessTac]
tuple [in CoqUniquenessTac]
tuple_rev [in CoqUniquenessTac]
U
union_map [in Metatheory]W
WSfun.disjoint [in FSetExtra]WSfun.elt [in CoqFSetInterface]
WSfun.Empty [in CoqFSetInterface]
WSfun.eq [in CoqFSetInterface]
WSfun.Equal [in CoqFSetInterface]
WSfun.Exists [in CoqFSetInterface]
WSfun.For_all [in CoqFSetInterface]
WSfun.fresh_list [in FSetExtra]
WSfun.notin [in FSetExtra]
WSfun.Subset [in CoqFSetInterface]
Record Index
E
EqDec_eq [in CoqEqDec]| 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 | (799 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 | (37 entries) |
| Module 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 | (32 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 | (171 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 | (23 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 | (117 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) |
| 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 | (261 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 | (1 entry) |
| 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 | (6 entries) |
| 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 | (26 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 | (2 entries) |
| Abbreviation 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 | (45 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 | (56 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) |
This page has been generated by coqdoc


WHAT WE DO
Startup Consulting
We work with you to identify critical next steps in getting your startup up and running in the most efficient manner and more importantly execute with you to minimize missteps and do overs. We help entrepreneurs, innovators, startups, and incubators launch new businesses, enter new markets and commercialize breakthrough ideas.
Tagline
- Developing Strategic Systems and Processes for Turning Ideas into Growth and Scaling Growth is what we do.
Competences
- New Market Entry
- 30|60|90 Strategy
- Idea Modelling
- Technology & Digital Business Experience DBX
- Logistics and Supply Chain Management
- Marketing & Sales Automation
Business Research and Analysis
It has become very crucial to be able to rapidly process, manage and make business sense of the abundance of information in today’s commercial environment. This is necessary to be able to make adjustments to strategy or even promptly take advantage of developing opportunities. Kani Partners provides frameworks for collating and analysing both internal and external business information and drawing actionable insights.
Tagline
-
Providing researched data and insight to business questions around
- Market Opportunities,
- Competitor & Trend Insight and
- Growth & Expansion Data.
Competences
- Market Opportunities
- Competitor & Trend Insight
- Growth & Expansion Data
Talent Strategy
The best strategy can fail if it is executed by the wrong set of people, we will work you through
not just developing the optimal strategy for your business goals but also locate an hire the resources
best suited to executing the strategy.
Our approach focuses on your whole business and talent strategy by the Kani group is about providing a clear and
coherent strategy that is linked to your organization’s business plan.
This way, you get an actionable plan that can be immediately implemented by your organisation and
also caters for future growth and expansion.
Assess and implement a more effective organizational design. Apply workforce planning and analytics.
Develop talent through career and performance management processes. Define your employee value
proposition through the development of an engaging culture. Identify key talents and build succession slates.
Tagline
- A company is only as great as its talent. Conversely, a company dies after it's talent
base gets too weak to sustain it's desired growth. A company’s talent is only as good as
its talent strategy.
HR heads and Talent leaders are finding it harder to manage the increasing with haphazard hiring and ineffective career management scenarios around their companies. Employees today aren’t interested in just jobs - they want meaningful careers - and most companies within Africa are not able to manage doing their core business and same time actualizing the career goals and dreams of their workforce. We have solutions to mitigate this.
Competences
- Workforce Planning
- Employee Engagement
- Hiring and Talent Pipeline Development
- Retreats and Brainstorming Planning
Process Optimization and Automation
We help organizations identify, rethink and automate business processes, minimizing the resources required to get the outputs of those process while significantly increasing the efficiency of the process and your employees.
Tagline
- The bigger companies grow, the harder it is to push through changes that use to be easier to make in the past,
the less adaptive they get to new processes and ways of working. Why? Complexities.
- Complexity, as measured by the number of requirements companies have to satisfy, is rising steadily. To make decisions and create a change, companies often set up a dedicated function, create a new process or report, and then build systems to coordinate with existing functions and sections of the business. This leads to an increase in organizational complicatedness; the number of procedures, vertical layers, interface structures, coordination bodies, and decision approvals have blown up. All of these internal complexities have seen companies hitherto working smart and changing fast to essentially slow down pace and growth a lot less. We aim to solve.
Competences
- Identify
- ReThink
- Automate (Technology Adoption & Complete Process Change, Process Improvement or Re-Structuring, Business Process Automation (BPA) [eg Customer Support, Social Media Management])
- Creativity and Disruptive Innovation
- Turn Around Management


I had been working as an Graphic Designer for 10 years before I switched to a new profession - Web Developer. I love it. If only I had done it earlier.
I am highly-motivated, result oriented, self-driven, hard-working, fast learner and smart eager to be a part of the team, learn new technologies, become a valuable employee of the company and bring it success.
Well-organized with an ability to prioritize tasks and capability to work, develop and grow in the company. Experienced in communicating with the team and clients. Attentive and accurate to details.
A talented graduate developer with a strong academic background and some commercial experience. A confident communicator, strategic thinker, and innovative creator to develop software that is customized to meet a company’s organizational needs, highlight their core competencies, and further their success.
If you like my work and have some cool project to work on, just send me a direct message or contact me through the phone.
TravelPharm is New Zealand company specializing in health supplements and organic, natural skincare products.
Website
Wordpress, JavaScript, HTML, CSS
TravelPharm
Beecology brings together and celebrates all that is great about New Zealand premium honey.
Ecommerce Website
Wordpress, JavaScript, HTML, CSS, WooCommerce
Beecology
GSENZ is a New Zealand brand specializing in Grape Seed Extract products which owned and operated by NATORG International Limited.
Ecommerce Website
Wordpress, JavaScript, HTML, CSS, WooCommerce
GSENZ
DIVINZ is a premium brand focusing on face mask collection.
Ecommerce Website
Wordpress, JavaScript, HTML, CSS, WooCommerce
DIVINZ
Scopes is a system website for finding and booking doctors, pharmacy and health related place.
Booking & Blogging Website
PHP, Bootstrap, SQL, JavaScript, HTML, CSS, Laravel
Scopes


UDEVADM
Section: udevadm (8)Updated: 11/10/2009
Index Return to Main Contents
NAME
udevadm - udev management toolSYNOPSIS
-
udevadm [--debug] [--version] [--help]
- udevadm info options
- udevadm trigger [options]
- udevadm settle [options]
- udevadm control command
- udevadm monitor [options]
- udevadm test [options] devpath
- udevadm info options
DESCRIPTION
OPTIONS
--debug
- Print debug messages to stderr.
--version
- Print version number.
--help
- Print help text.
udevadm info options
Queries the udev database for device information stored in the udev database. It can also query the properties of a device from its sysfs representation to help creating udev rules that match this device.
--query=type
- Query the database for specified type of device data. It needs the --path or --name to identify the specified device. Valid queries are: name, symlink, path, property, all.
--path=devpath
- The devpath of the device to query.
--name=file
- The name of the device node or a symlink to query
--root
- The udev root directory: /dev. If used in conjunction with a name or symlink query, the query returns the absolute path including the root directory.
--attribute-walk
- Print all sysfs properties of the specified device that can be used in udev rules to match the specified device. It prints all devices along the chain, up to the root of sysfs that can be used in udev rules.
--device-id-of-file=file
- Print major/minor numbers of the underlying device, where the file lives on.
--export-db
- Export the content of the udev database.
--version
- Print version.
--help
- Print help text.
udevadm trigger [options]
Request device events from the kernel. Usually used to replay events at system coldplug time.
--verbose
- Print the list of devices which will be triggered.
--dry-run
- Do not actually trigger the event.
--type=type
- Trigger a specific type of devices. Valid types are: devices, subsystems, failed. The default value is devices.
--action=action
- Type of event to be triggered. The default value is add.
--subsystem-match=subsystem
- Trigger events for devices which belong to a matching subsystem. This option can be specified multiple times and supports shell style pattern matching.
--subsystem-nomatch=subsystem
- Do not trigger events for devices which belong to a matching subsystem. This option can be specified multiple times and supports shell style pattern matching.
--attr-match=attribute=value
- Trigger events for devices with a matching sysfs attribute. If a value is specified along with the attribute name, the content of the attribute is matched against the given value using shell style pattern matching. If no value is specified, the existence of the sysfs attribute is checked. This option can be specified multiple times.
--attr-nomatch=attribute=value
- Do not trigger events for devices with a matching sysfs attribute. If a value is specified along with the attribute name, the content of the attribute is matched against the given value using shell style pattern matching. If no value is specified, the existence of the sysfs attribute is checked. This option can be specified multiple times.
--property-match=property=value
- Trigger events for devices with a matching property value. This option can be specified multiple times and supports shell style pattern matching.
--sysname-match=name
- Trigger events for devices with a matching sys device name. This option can be specified multiple times and supports shell style pattern matching.
udevadm settle [options]
Watches the udev event queue, and exits if all current events are handled.
--timeout=seconds
- Maximum number of seconds to wait for the event queue to become empty. The default value is 180 seconds. A value of 0 will check if the queue is empty and always return immediately.
--seq-start=seqnum
- Wait only for events after the given sequence number.
--seq-end=seqnum
- Wait only for events before the given sequence number.
--exit-if-exists=file
- Stop waiting if file exists.
--quiet
- Do not print any output, like the remaining queue entries when reaching the timeout.
--help
- Print help text.
udevadm control command
Modify the internal state of the running udev daemon.
--log-priority=value
- Set the internal log level of udevd. Valid values are the numerical syslog priorities or their textual representations: err, info and debug.
--stop-exec-queue
- Signal udevd to stop executing new events. Incoming events will be queued.
--start-exec-queue
- Signal udevd to enable the execution of events.
--reload-rules
- Signal udevd to reload the rules files. The udev daemon detects changes automatically, this option is usually not needed. Reloading rules does not apply any changes to already existing devices.
--property=KEY=value
- Set a global property for all events.
--max-childs=value
- Set the maximum number of events, udevd will handle at the same time.
--help
- Print help text.
udevadm monitor [options]
Listens to the kernel uevents and events sent out by a udev rule and prints the devpath of the event to the console. It can be used to analyze the event timing, by comparing the timestamps of the kernel uevent and the udev event.
--kernel
- Print the kernel uevents.
--udev
- Print the udev event after the rule processing.
--property
- Also print the properties of the event.
--help
- Print help text.
udevadm test [options] devpath
Simulate a udev event run for the given device, and print debug output.
--action=string
- The action string.
--subsystem=string
- The subsystem string.
--help
- Print help text.
AUTHOR
Written by Kay Sievers<EMAIL_ADDRESS>SEE ALSO
Index
This document was created by man2html, using the manual pages.
Time: 05:34:31 GMT, December 24, 2015