Skip to content

Latest commit

 

History

History
47 lines (45 loc) · 2.31 KB

index.md

File metadata and controls

47 lines (45 loc) · 2.31 KB
Raw

Index to the Coq Definitions

Follows an index of all Coq definitions (including inductive types, lemmas, theorems, etc.) used in the text:

  • Figure 1: Inductive LE in file lua.v
  • Figure 2: Inductive Lstep in file lua.v
  • Figure 3: Definition example in file example.v
  • Figure 4: Inductive PType, Inductive PE in file pallene.v
  • Figure 5: Inductive PTyping in file pallene.v
  • Figure 6: Inductive pstep in file pallene.v
  • Figure 7: Fixpoint vcast in file pallene.v
  • Figure 8: Fixpoint Pall2Lua in file lua.v
  • Theorem 1: Theorem Progress in file pallene.v
  • Theorem 2: Corollary PPreservation in file pallene.v
  • Figure 9: Inductive IRType, Inductive Value, Inductive IRE in file lir.v
  • Figure 10: Inductive IRTyping in file lir.v
  • Figure 11: Inductive step in file lir.v
  • Theorem 3: Theorem Progress in file lir.v
  • Theorem 4: Theorem Preservation in file lir.v
  • Figure 12: Fixpoint Lua2Lir in file lua.v
  • Lemma 5: Theorem Lua2LirTypeAux in file lua.v
  • Lemma 6: Theorem L2LirValue in file lua.v
  • Theorem 7: Theorem SimLua in file lua.v
  • Figure 13a: Definition PT2IRT in file pall2lir.v
  • Figure 13b: Definition Cast in file pall2lir.v
  • Figure 13c: Fixpoint Pall2Lir in file pall2lir.v
  • Lemma 8: Theorem Pall2LirWellTyped in file pall2lir.v
  • Lemma 9: Theorem PValueValue in file pall2lir.v
  • Theorem 10: Theorem SimPallLir in file pall2lir.v
  • Theorem 11: Theorem SimPallLirF in file pall2lir.v
  • Figure 14: Fixpoint dyn in file dyn.v
  • Lemma 13: Theorem dynTyping in file dyn.v
  • Theorem 14: Theorem PallLua in file lua.v
  • Lemma 15: Theorem dynIdempotent in file dyn.v
  • Lemma 16: Theorem LuaIsDyn in file lua.v
  • Lemma 17: Theorem dynValue in file dyn.v
  • Lemma 18: Lemma ValueStar in file dyn.v
  • Theorem 19: Corollary SimDyn in file simprec.v
  • Figure 15: Inductive TPrecision in file precision.v
  • Figure 16: Inductive Precision in file precision.v
  • Lemma 20: Lemma PrecisionRefl, Lemma PrecTrans in file precision.v
  • Lemma 21: Theorem DynLessPrecise in file precision.v
  • Lemma 22: Theorem PrecDynEqual in file precision.v
  • Theorem 23: Theorem SimMult in file simprec.v
  • Lemma 24: Corollary CatchUpP in file simprec.v
  • Lemma 25: Theorem Sim in file simprec.v