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 | (73 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 | (17 entries) |

Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 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 | (26 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 | (12 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 | (5 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 | (11 entries) |

# Global Index

## A

assertion [definition, in Hoare]Assign [constructor, in ImpSimpl]

## B

beval [definition, in ImpSimpl]bexp [inductive, in ImpSimpl]

## C

cmd [inductive, in ImpSimpl]completeness [lemma, in Hoare]

Const [constructor, in ImpSimpl]

## E

Equal [constructor, in ImpSimpl]eval [definition, in ImpSimpl]

ExAssign [constructor, in ImpSimpl]

exec [inductive, in ImpSimpl]

ExIfFalse [constructor, in ImpSimpl]

ExIfTrue [constructor, in ImpSimpl]

exp [inductive, in ImpSimpl]

ExSeq [constructor, in ImpSimpl]

ExSkip [constructor, in ImpSimpl]

ExWhileFalse [constructor, in ImpSimpl]

ExWhileTrue [constructor, in ImpSimpl]

## H

himpl [definition, in Hoare]Hoare [library]

hoare_triple_sound [lemma, in Hoare]

hoare_triple_big_step_while [lemma, in Hoare]

hoare_triple [inductive, in Hoare]

hoare_valid [definition, in Hoare]

hoare_interp [definition, in Hoare]

HtAssign [constructor, in Hoare]

HtConsequence [constructor, in Hoare]

HtExists [constructor, in Hoare]

HtIf [constructor, in Hoare]

HtSeq [constructor, in Hoare]

HtSkip [constructor, in Hoare]

HtStrengthenPost [lemma, in Hoare]

HtWeakenPre [lemma, in Hoare]

HtWhileInv [constructor, in Hoare]

## I

If_ [constructor, in ImpSimpl]ImpSimpl [library]

## L

Less [constructor, in ImpSimpl]## M

Minus [constructor, in ImpSimpl]Mult [constructor, in ImpSimpl]

## P

Plus [constructor, in ImpSimpl]## S

Seq [constructor, in ImpSimpl]set [definition, in ImpSimpl]

Skip [constructor, in ImpSimpl]

## V

valuation [definition, in ImpSimpl]var [definition, in ImpSimpl]

Var [constructor, in ImpSimpl]

## W

WeP [definition, in Hoare]While_ [constructor, in ImpSimpl]

wpl [definition, in Hoare]

wpl_soundness_synt [lemma, in Hoare]

wpl_mon [lemma, in Hoare]

wpl_entailment' [lemma, in Hoare]

wpl_entailment [lemma, in Hoare]

wpl_complete_sem' [lemma, in Hoare]

wpl_complete_sem [lemma, in Hoare]

wpl_sound_sem [lemma, in Hoare]

## other

_ ;; _ (cmd_scope) [notation, in ImpSimpl]_ <- _ (cmd_scope) [notation, in ImpSimpl]

_ < _ (cmd_scope) [notation, in ImpSimpl]

_ = _ (cmd_scope) [notation, in ImpSimpl]

_ * _ (cmd_scope) [notation, in ImpSimpl]

_ - _ (cmd_scope) [notation, in ImpSimpl]

_ + _ (cmd_scope) [notation, in ImpSimpl]

_ < _ (reset_scope) [notation, in ImpSimpl]

_ = _ (reset_scope) [notation, in ImpSimpl]

_ * _ (reset_scope) [notation, in ImpSimpl]

_ - _ (reset_scope) [notation, in ImpSimpl]

_ + _ (reset_scope) [notation, in ImpSimpl]

_ $! _ [notation, in ImpSimpl]

_ ==> _ [notation, in Hoare]

when _ then _ else _ done [notation, in ImpSimpl]

{{ _ }} while _ loop _ done [notation, in ImpSimpl]

{{ _ }} _ {{ _ }} [notation, in Hoare]

# Notation Index

## other

_ ;; _ (cmd_scope) [in ImpSimpl]_ <- _ (cmd_scope) [in ImpSimpl]

_ < _ (cmd_scope) [in ImpSimpl]

_ = _ (cmd_scope) [in ImpSimpl]

_ * _ (cmd_scope) [in ImpSimpl]

_ - _ (cmd_scope) [in ImpSimpl]

_ + _ (cmd_scope) [in ImpSimpl]

_ < _ (reset_scope) [in ImpSimpl]

_ = _ (reset_scope) [in ImpSimpl]

_ * _ (reset_scope) [in ImpSimpl]

_ - _ (reset_scope) [in ImpSimpl]

_ + _ (reset_scope) [in ImpSimpl]

_ $! _ [in ImpSimpl]

_ ==> _ [in Hoare]

when _ then _ else _ done [in ImpSimpl]

{{ _ }} while _ loop _ done [in ImpSimpl]

{{ _ }} _ {{ _ }} [in Hoare]

# Library Index

## H

Hoare## I

ImpSimpl# Constructor Index

## A

Assign [in ImpSimpl]## C

Const [in ImpSimpl]## E

Equal [in ImpSimpl]ExAssign [in ImpSimpl]

ExIfFalse [in ImpSimpl]

ExIfTrue [in ImpSimpl]

ExSeq [in ImpSimpl]

ExSkip [in ImpSimpl]

ExWhileFalse [in ImpSimpl]

ExWhileTrue [in ImpSimpl]

## H

HtAssign [in Hoare]HtConsequence [in Hoare]

HtExists [in Hoare]

HtIf [in Hoare]

HtSeq [in Hoare]

HtSkip [in Hoare]

HtWhileInv [in Hoare]

## I

If_ [in ImpSimpl]## L

Less [in ImpSimpl]## M

Minus [in ImpSimpl]Mult [in ImpSimpl]

## P

Plus [in ImpSimpl]## S

Seq [in ImpSimpl]Skip [in ImpSimpl]

## V

Var [in ImpSimpl]## W

While_ [in ImpSimpl]# Lemma Index

## C

completeness [in Hoare]## H

hoare_triple_sound [in Hoare]hoare_triple_big_step_while [in Hoare]

HtStrengthenPost [in Hoare]

HtWeakenPre [in Hoare]

## W

wpl_soundness_synt [in Hoare]wpl_mon [in Hoare]

wpl_entailment' [in Hoare]

wpl_entailment [in Hoare]

wpl_complete_sem' [in Hoare]

wpl_complete_sem [in Hoare]

wpl_sound_sem [in Hoare]

# Inductive Index

## B

bexp [in ImpSimpl]## C

cmd [in ImpSimpl]## E

exec [in ImpSimpl]exp [in ImpSimpl]

## H

hoare_triple [in Hoare]# Definition Index

## A

assertion [in Hoare]## B

beval [in ImpSimpl]## E

eval [in ImpSimpl]## H

himpl [in Hoare]hoare_valid [in Hoare]

hoare_interp [in Hoare]

## S

set [in ImpSimpl]## V

valuation [in ImpSimpl]var [in ImpSimpl]

## W

WeP [in Hoare]wpl [in Hoare]

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 | (73 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 | (17 entries) |

Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 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 | (26 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 | (12 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 | (5 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 | (11 entries) |

This page has been generated by coqdoc