| 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 | (137 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 | (6 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 | (22 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 | (5 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 | (25 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 | (36 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 | (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 | (9 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 | (22 entries) |
Global Index
E
enum_3N_stupid [lemma, in HoareTut.exgcd]enum_3N [definition, in HoareTut.exgcd]
Example [module, in HoareTut.exgcd]
Example.binop [constructor, in HoareTut.exgcd]
Example.binOP [inductive, in HoareTut.exgcd]
Example.const [constructor, in HoareTut.exgcd]
Example.Env [definition, in HoareTut.exgcd]
Example.EQ [constructor, in HoareTut.exgcd]
Example.eval [definition, in HoareTut.exgcd]
Example.eval_relOP [definition, in HoareTut.exgcd]
Example.eval_binOP [definition, in HoareTut.exgcd]
Example.ExExpr [inductive, in HoareTut.exgcd]
Example.Expr [definition, in HoareTut.exgcd]
Example.ExVar [inductive, in HoareTut.exgcd]
Example.get [definition, in HoareTut.exgcd]
Example.getvar [constructor, in HoareTut.exgcd]
Example.LE [constructor, in HoareTut.exgcd]
Example.MINUS [constructor, in HoareTut.exgcd]
Example.NEQ [constructor, in HoareTut.exgcd]
Example.PLUS [constructor, in HoareTut.exgcd]
Example.relop [constructor, in HoareTut.exgcd]
Example.relOP [inductive, in HoareTut.exgcd]
Example.upd [definition, in HoareTut.exgcd]
Example.Var [definition, in HoareTut.exgcd]
Example.VX [constructor, in HoareTut.exgcd]
Example.VY [constructor, in HoareTut.exgcd]
exgcd [library]
ExprLang [module, in HoareTut.hoarelogicsemantics]
ExprLang.Env [axiom, in HoareTut.hoarelogicsemantics]
ExprLang.eval [axiom, in HoareTut.hoarelogicsemantics]
ExprLang.Expr [axiom, in HoareTut.hoarelogicsemantics]
ExprLang.upd [axiom, in HoareTut.hoarelogicsemantics]
ExprLang.Var [axiom, in HoareTut.hoarelogicsemantics]
G
gcd [definition, in HoareTut.exgcd]gcd_total_proof [lemma, in HoareTut.exgcd]
gcd_partial_proof [lemma, in HoareTut.exgcd]
H
HL [module, in HoareTut.exgcd]HoareLogic [module, in HoareTut.hoarelogic]
hoarelogic [library]
HoareLogicDefs [module, in HoareTut.hoarelogicsemantics]
HoareLogicDefs.E [module, in HoareTut.hoarelogicsemantics]
HoareLogicDefs.exec [inductive, in HoareTut.hoarelogicsemantics]
HoareLogicDefs.exec_Iif_false [axiom, in HoareTut.hoarelogicsemantics]
HoareLogicDefs.exec_Iif_true [axiom, in HoareTut.hoarelogicsemantics]
HoareLogicDefs.exec_Iwhile [constructor, in HoareTut.hoarelogicsemantics]
HoareLogicDefs.exec_Iseq [constructor, in HoareTut.hoarelogicsemantics]
HoareLogicDefs.exec_Iif [constructor, in HoareTut.hoarelogicsemantics]
HoareLogicDefs.exec_Iset [constructor, in HoareTut.hoarelogicsemantics]
HoareLogicDefs.exec_Iskip [constructor, in HoareTut.hoarelogicsemantics]
HoareLogicDefs.Iif [constructor, in HoareTut.hoarelogicsemantics]
HoareLogicDefs.ImpProg [inductive, in HoareTut.hoarelogicsemantics]
HoareLogicDefs.Iseq [constructor, in HoareTut.hoarelogicsemantics]
HoareLogicDefs.Iset [constructor, in HoareTut.hoarelogicsemantics]
HoareLogicDefs.Iskip [constructor, in HoareTut.hoarelogicsemantics]
HoareLogicDefs.Iwhile [constructor, in HoareTut.hoarelogicsemantics]
HoareLogicDefs.Pred [definition, in HoareTut.hoarelogicsemantics]
HoareLogicDefs.wlp [definition, in HoareTut.hoarelogicsemantics]
HoareLogicDefs.wp [definition, in HoareTut.hoarelogicsemantics]
_ [= _ =] [notation, in HoareTut.hoarelogicsemantics]
_ {= _ =} [notation, in HoareTut.hoarelogicsemantics]
_ |= _ [notation, in HoareTut.hoarelogicsemantics]
HoareLogicSem [module, in HoareTut.hoarelogicsemantics]
hoarelogicsemantics [library]
HoareLogicSem.E [module, in HoareTut.hoarelogicsemantics]
HoareLogicSem.HLD [module, in HoareTut.hoarelogicsemantics]
HoareLogicSem.PHL [module, in HoareTut.hoarelogicsemantics]
HoareLogicSem.THL [module, in HoareTut.hoarelogicsemantics]
HoareLogicSem.wp_entails_wlp [axiom, in HoareTut.hoarelogicsemantics]
HoareLogic.E [module, in HoareTut.hoarelogic]
HoareLogic.HLD [module, in HoareTut.hoarelogic]
HoareLogic.HLD.E [module, in HoareTut.hoarelogic]
HoareLogic.HLD.exec [inductive, in HoareTut.hoarelogic]
HoareLogic.HLD.exec_Iif_false [lemma, in HoareTut.hoarelogic]
HoareLogic.HLD.exec_Iif_true [lemma, in HoareTut.hoarelogic]
HoareLogic.HLD.exec_Iwhile [constructor, in HoareTut.hoarelogic]
HoareLogic.HLD.exec_Iseq [constructor, in HoareTut.hoarelogic]
HoareLogic.HLD.exec_Iif [constructor, in HoareTut.hoarelogic]
HoareLogic.HLD.exec_Iset [constructor, in HoareTut.hoarelogic]
HoareLogic.HLD.exec_Iskip [constructor, in HoareTut.hoarelogic]
HoareLogic.HLD.Iif [constructor, in HoareTut.hoarelogic]
HoareLogic.HLD.ImpProg [inductive, in HoareTut.hoarelogic]
HoareLogic.HLD.Iseq [constructor, in HoareTut.hoarelogic]
HoareLogic.HLD.Iset [constructor, in HoareTut.hoarelogic]
HoareLogic.HLD.Iskip [constructor, in HoareTut.hoarelogic]
HoareLogic.HLD.Iwhile [constructor, in HoareTut.hoarelogic]
HoareLogic.HLD.Pred [definition, in HoareTut.hoarelogic]
HoareLogic.HLD.wlp [definition, in HoareTut.hoarelogic]
HoareLogic.HLD.wp [definition, in HoareTut.hoarelogic]
_ [= _ =] [notation, in HoareTut.hoarelogic]
_ {= _ =} [notation, in HoareTut.hoarelogic]
_ |= _ [notation, in HoareTut.hoarelogic]
HoareLogic.PHL [module, in HoareTut.hoarelogic]
HoareLogic.THL [module, in HoareTut.hoarelogic]
HoareLogic.wp_entails_wlp [lemma, in HoareTut.hoarelogic]
HoareProofSystem [module, in HoareTut.hoarelogicsemantics]
HoareProofSystem.completeness [axiom, in HoareTut.hoarelogicsemantics]
HoareProofSystem.HLD [module, in HoareTut.hoarelogicsemantics]
HoareProofSystem.sem_wp [axiom, in HoareTut.hoarelogicsemantics]
HoareProofSystem.soundness [axiom, in HoareTut.hoarelogicsemantics]
HoareProofSystem.synt_wp [axiom, in HoareTut.hoarelogicsemantics]
P
PartialHoareLogic [module, in HoareTut.partialhoarelogic]partialhoarelogic [library]
PartialHoareLogic.completeness [lemma, in HoareTut.partialhoarelogic]
PartialHoareLogic.HLD [module, in HoareTut.partialhoarelogic]
PartialHoareLogic.sem_wp [definition, in HoareTut.partialhoarelogic]
PartialHoareLogic.soundness [lemma, in HoareTut.partialhoarelogic]
PartialHoareLogic.synt_wp_monotonic [lemma, in HoareTut.partialhoarelogic]
PartialHoareLogic.synt_wp [definition, in HoareTut.partialhoarelogic]
PartialHoareLogic.wp_complete [lemma, in HoareTut.partialhoarelogic]
PartialHoareLogic.wp_sound [lemma, in HoareTut.partialhoarelogic]
T
TotalHoareLogic [module, in HoareTut.totalhoarelogic]totalhoarelogic [library]
TotalHoareLogic.aux_wlp [definition, in HoareTut.totalhoarelogic]
TotalHoareLogic.completeness [lemma, in HoareTut.totalhoarelogic]
TotalHoareLogic.execn [inductive, in HoareTut.totalhoarelogic]
TotalHoareLogic.execn_Iwhile [constructor, in HoareTut.totalhoarelogic]
TotalHoareLogic.execn_Iseq [constructor, in HoareTut.totalhoarelogic]
TotalHoareLogic.execn_Iif [constructor, in HoareTut.totalhoarelogic]
TotalHoareLogic.execn_Iset [constructor, in HoareTut.totalhoarelogic]
TotalHoareLogic.execn_Iskip [constructor, in HoareTut.totalhoarelogic]
TotalHoareLogic.exec_execn [lemma, in HoareTut.totalhoarelogic]
TotalHoareLogic.exec_deterministic [lemma, in HoareTut.totalhoarelogic]
TotalHoareLogic.exec_test_inversion [lemma, in HoareTut.totalhoarelogic]
TotalHoareLogic.exec_inversion [lemma, in HoareTut.totalhoarelogic]
TotalHoareLogic.HLD [module, in HoareTut.totalhoarelogic]
TotalHoareLogic.reduces [definition, in HoareTut.totalhoarelogic]
TotalHoareLogic.reduces_wf [lemma, in HoareTut.totalhoarelogic]
TotalHoareLogic.sem_wp [definition, in HoareTut.totalhoarelogic]
TotalHoareLogic.soundness [lemma, in HoareTut.totalhoarelogic]
TotalHoareLogic.synt_wp_conj [lemma, in HoareTut.totalhoarelogic]
TotalHoareLogic.synt_wp_monotonic [lemma, in HoareTut.totalhoarelogic]
TotalHoareLogic.synt_wp [definition, in HoareTut.totalhoarelogic]
TotalHoareLogic.wp_complete [lemma, in HoareTut.totalhoarelogic]
TotalHoareLogic.wp_sound [lemma, in HoareTut.totalhoarelogic]
Z
Zgcd_minus [lemma, in HoareTut.exgcd]Zneq_bool_true [lemma, in HoareTut.exgcd]
Zneq_bool_false [lemma, in HoareTut.exgcd]
Notation Index
H
_ [= _ =] [in HoareTut.hoarelogicsemantics]_ {= _ =} [in HoareTut.hoarelogicsemantics]
_ |= _ [in HoareTut.hoarelogicsemantics]
_ [= _ =] [in HoareTut.hoarelogic]
_ {= _ =} [in HoareTut.hoarelogic]
_ |= _ [in HoareTut.hoarelogic]
Module Index
E
Example [in HoareTut.exgcd]ExprLang [in HoareTut.hoarelogicsemantics]
H
HL [in HoareTut.exgcd]HoareLogic [in HoareTut.hoarelogic]
HoareLogicDefs [in HoareTut.hoarelogicsemantics]
HoareLogicDefs.E [in HoareTut.hoarelogicsemantics]
HoareLogicSem [in HoareTut.hoarelogicsemantics]
HoareLogicSem.E [in HoareTut.hoarelogicsemantics]
HoareLogicSem.HLD [in HoareTut.hoarelogicsemantics]
HoareLogicSem.PHL [in HoareTut.hoarelogicsemantics]
HoareLogicSem.THL [in HoareTut.hoarelogicsemantics]
HoareLogic.E [in HoareTut.hoarelogic]
HoareLogic.HLD [in HoareTut.hoarelogic]
HoareLogic.HLD.E [in HoareTut.hoarelogic]
HoareLogic.PHL [in HoareTut.hoarelogic]
HoareLogic.THL [in HoareTut.hoarelogic]
HoareProofSystem [in HoareTut.hoarelogicsemantics]
HoareProofSystem.HLD [in HoareTut.hoarelogicsemantics]
P
PartialHoareLogic [in HoareTut.partialhoarelogic]PartialHoareLogic.HLD [in HoareTut.partialhoarelogic]
T
TotalHoareLogic [in HoareTut.totalhoarelogic]TotalHoareLogic.HLD [in HoareTut.totalhoarelogic]
Library Index
E
exgcdH
hoarelogichoarelogicsemantics
P
partialhoarelogicT
totalhoarelogicLemma Index
E
enum_3N_stupid [in HoareTut.exgcd]G
gcd_total_proof [in HoareTut.exgcd]gcd_partial_proof [in HoareTut.exgcd]
H
HoareLogic.HLD.exec_Iif_false [in HoareTut.hoarelogic]HoareLogic.HLD.exec_Iif_true [in HoareTut.hoarelogic]
HoareLogic.wp_entails_wlp [in HoareTut.hoarelogic]
P
PartialHoareLogic.completeness [in HoareTut.partialhoarelogic]PartialHoareLogic.soundness [in HoareTut.partialhoarelogic]
PartialHoareLogic.synt_wp_monotonic [in HoareTut.partialhoarelogic]
PartialHoareLogic.wp_complete [in HoareTut.partialhoarelogic]
PartialHoareLogic.wp_sound [in HoareTut.partialhoarelogic]
T
TotalHoareLogic.completeness [in HoareTut.totalhoarelogic]TotalHoareLogic.exec_execn [in HoareTut.totalhoarelogic]
TotalHoareLogic.exec_deterministic [in HoareTut.totalhoarelogic]
TotalHoareLogic.exec_test_inversion [in HoareTut.totalhoarelogic]
TotalHoareLogic.exec_inversion [in HoareTut.totalhoarelogic]
TotalHoareLogic.reduces_wf [in HoareTut.totalhoarelogic]
TotalHoareLogic.soundness [in HoareTut.totalhoarelogic]
TotalHoareLogic.synt_wp_conj [in HoareTut.totalhoarelogic]
TotalHoareLogic.synt_wp_monotonic [in HoareTut.totalhoarelogic]
TotalHoareLogic.wp_complete [in HoareTut.totalhoarelogic]
TotalHoareLogic.wp_sound [in HoareTut.totalhoarelogic]
Z
Zgcd_minus [in HoareTut.exgcd]Zneq_bool_true [in HoareTut.exgcd]
Zneq_bool_false [in HoareTut.exgcd]
Constructor Index
E
Example.binop [in HoareTut.exgcd]Example.const [in HoareTut.exgcd]
Example.EQ [in HoareTut.exgcd]
Example.getvar [in HoareTut.exgcd]
Example.LE [in HoareTut.exgcd]
Example.MINUS [in HoareTut.exgcd]
Example.NEQ [in HoareTut.exgcd]
Example.PLUS [in HoareTut.exgcd]
Example.relop [in HoareTut.exgcd]
Example.VX [in HoareTut.exgcd]
Example.VY [in HoareTut.exgcd]
H
HoareLogicDefs.exec_Iwhile [in HoareTut.hoarelogicsemantics]HoareLogicDefs.exec_Iseq [in HoareTut.hoarelogicsemantics]
HoareLogicDefs.exec_Iif [in HoareTut.hoarelogicsemantics]
HoareLogicDefs.exec_Iset [in HoareTut.hoarelogicsemantics]
HoareLogicDefs.exec_Iskip [in HoareTut.hoarelogicsemantics]
HoareLogicDefs.Iif [in HoareTut.hoarelogicsemantics]
HoareLogicDefs.Iseq [in HoareTut.hoarelogicsemantics]
HoareLogicDefs.Iset [in HoareTut.hoarelogicsemantics]
HoareLogicDefs.Iskip [in HoareTut.hoarelogicsemantics]
HoareLogicDefs.Iwhile [in HoareTut.hoarelogicsemantics]
HoareLogic.HLD.exec_Iwhile [in HoareTut.hoarelogic]
HoareLogic.HLD.exec_Iseq [in HoareTut.hoarelogic]
HoareLogic.HLD.exec_Iif [in HoareTut.hoarelogic]
HoareLogic.HLD.exec_Iset [in HoareTut.hoarelogic]
HoareLogic.HLD.exec_Iskip [in HoareTut.hoarelogic]
HoareLogic.HLD.Iif [in HoareTut.hoarelogic]
HoareLogic.HLD.Iseq [in HoareTut.hoarelogic]
HoareLogic.HLD.Iset [in HoareTut.hoarelogic]
HoareLogic.HLD.Iskip [in HoareTut.hoarelogic]
HoareLogic.HLD.Iwhile [in HoareTut.hoarelogic]
T
TotalHoareLogic.execn_Iwhile [in HoareTut.totalhoarelogic]TotalHoareLogic.execn_Iseq [in HoareTut.totalhoarelogic]
TotalHoareLogic.execn_Iif [in HoareTut.totalhoarelogic]
TotalHoareLogic.execn_Iset [in HoareTut.totalhoarelogic]
TotalHoareLogic.execn_Iskip [in HoareTut.totalhoarelogic]
Axiom Index
E
ExprLang.Env [in HoareTut.hoarelogicsemantics]ExprLang.eval [in HoareTut.hoarelogicsemantics]
ExprLang.Expr [in HoareTut.hoarelogicsemantics]
ExprLang.upd [in HoareTut.hoarelogicsemantics]
ExprLang.Var [in HoareTut.hoarelogicsemantics]
H
HoareLogicDefs.exec_Iif_false [in HoareTut.hoarelogicsemantics]HoareLogicDefs.exec_Iif_true [in HoareTut.hoarelogicsemantics]
HoareLogicSem.wp_entails_wlp [in HoareTut.hoarelogicsemantics]
HoareProofSystem.completeness [in HoareTut.hoarelogicsemantics]
HoareProofSystem.sem_wp [in HoareTut.hoarelogicsemantics]
HoareProofSystem.soundness [in HoareTut.hoarelogicsemantics]
HoareProofSystem.synt_wp [in HoareTut.hoarelogicsemantics]
Inductive Index
E
Example.binOP [in HoareTut.exgcd]Example.ExExpr [in HoareTut.exgcd]
Example.ExVar [in HoareTut.exgcd]
Example.relOP [in HoareTut.exgcd]
H
HoareLogicDefs.exec [in HoareTut.hoarelogicsemantics]HoareLogicDefs.ImpProg [in HoareTut.hoarelogicsemantics]
HoareLogic.HLD.exec [in HoareTut.hoarelogic]
HoareLogic.HLD.ImpProg [in HoareTut.hoarelogic]
T
TotalHoareLogic.execn [in HoareTut.totalhoarelogic]Definition Index
E
enum_3N [in HoareTut.exgcd]Example.Env [in HoareTut.exgcd]
Example.eval [in HoareTut.exgcd]
Example.eval_relOP [in HoareTut.exgcd]
Example.eval_binOP [in HoareTut.exgcd]
Example.Expr [in HoareTut.exgcd]
Example.get [in HoareTut.exgcd]
Example.upd [in HoareTut.exgcd]
Example.Var [in HoareTut.exgcd]
G
gcd [in HoareTut.exgcd]H
HoareLogicDefs.Pred [in HoareTut.hoarelogicsemantics]HoareLogicDefs.wlp [in HoareTut.hoarelogicsemantics]
HoareLogicDefs.wp [in HoareTut.hoarelogicsemantics]
HoareLogic.HLD.Pred [in HoareTut.hoarelogic]
HoareLogic.HLD.wlp [in HoareTut.hoarelogic]
HoareLogic.HLD.wp [in HoareTut.hoarelogic]
P
PartialHoareLogic.sem_wp [in HoareTut.partialhoarelogic]PartialHoareLogic.synt_wp [in HoareTut.partialhoarelogic]
T
TotalHoareLogic.aux_wlp [in HoareTut.totalhoarelogic]TotalHoareLogic.reduces [in HoareTut.totalhoarelogic]
TotalHoareLogic.sem_wp [in HoareTut.totalhoarelogic]
TotalHoareLogic.synt_wp [in HoareTut.totalhoarelogic]
| 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 | (137 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 | (6 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 | (22 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 | (5 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 | (25 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 | (36 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 | (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 | (9 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 | (22 entries) |
This page has been generated by coqdoc