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 | _ | (36 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 | _ | (18 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 | _ | (1 entry) |

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 | _ | (2 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (1 entry) |

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 | _ | (8 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 | _ | (5 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 | _ | (1 entry) |

# Global Index

## E

eqv [definition, in Mergesort]eqv_spec [lemma, in Mergesort]

## F

filter_app [lemma, in Mergesort]filter_empty [lemma, in Mergesort]

filter_sublist [lemma, in Mergesort]

flatten [definition, in Mergesort]

## L

le_not [lemma, in Mergesort]le_refl [lemma, in Mergesort]

## M

merge [definition, in Mergesort]mergesort [definition, in Mergesort]

Mergesort [library]

merge_iter [definition, in Mergesort]

merge_pairs [definition, in Mergesort]

merge_spec [lemma, in Mergesort]

## P

Permutation_NoDup [lemma, in Mergesort]presort [definition, in Mergesort]

## S

SORT [section, in Mergesort]Sorted [inductive, in Mergesort]

Sorted_cons [constructor, in Mergesort]

Sorted_nil [constructor, in Mergesort]

Sorted_1 [lemma, in Mergesort]

Sorted_2 [lemma, in Mergesort]

SORT.A [variable, in Mergesort]

SORT.le [variable, in Mergesort]

SORT.le_dec [variable, in Mergesort]

SORT.le_total [variable, in Mergesort]

SORT.le_trans [variable, in Mergesort]

Stable [definition, in Mergesort]

Stable_app [lemma, in Mergesort]

Stable_cons_app [lemma, in Mergesort]

Stable_cons_app' [lemma, in Mergesort]

Stable_decomp [lemma, in Mergesort]

Stable_refl [lemma, in Mergesort]

Stable_skip [lemma, in Mergesort]

Stable_swap [lemma, in Mergesort]

Stable_trans [lemma, in Mergesort]

# Lemma Index

## E

eqv_spec [in Mergesort]## F

filter_app [in Mergesort]filter_empty [in Mergesort]

filter_sublist [in Mergesort]

## L

le_not [in Mergesort]le_refl [in Mergesort]

## M

merge_spec [in Mergesort]## P

Permutation_NoDup [in Mergesort]## S

Sorted_1 [in Mergesort]Sorted_2 [in Mergesort]

Stable_app [in Mergesort]

Stable_cons_app [in Mergesort]

Stable_cons_app' [in Mergesort]

Stable_decomp [in Mergesort]

Stable_refl [in Mergesort]

Stable_skip [in Mergesort]

Stable_swap [in Mergesort]

Stable_trans [in Mergesort]

# Section Index

## S

SORT [in Mergesort]# Constructor Index

## S

Sorted_cons [in Mergesort]Sorted_nil [in Mergesort]

# Inductive Index

## S

Sorted [in Mergesort]# Definition Index

## E

eqv [in Mergesort]## F

flatten [in Mergesort]## M

merge [in Mergesort]mergesort [in Mergesort]

merge_iter [in Mergesort]

merge_pairs [in Mergesort]

## P

presort [in Mergesort]## S

Stable [in Mergesort]# Variable Index

## S

SORT.A [in Mergesort]SORT.le [in Mergesort]

SORT.le_dec [in Mergesort]

SORT.le_total [in Mergesort]

SORT.le_trans [in Mergesort]

# Library Index

## M

MergesortGlobal 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 | _ | (36 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 | _ | (18 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 | _ | (1 entry) |

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 | _ | (2 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (1 entry) |

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 | _ | (8 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 | _ | (5 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 | _ | (1 entry) |

This page has been generated by coqdoc