Skip to content

Commit

Permalink
Test out modifying the GUIDE to use coqdoc
Browse files Browse the repository at this point in the history
  • Loading branch information
audreyseo committed Jun 1, 2024
1 parent a57f960 commit 34e5d7c
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion GUIDE.md
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
## Claims

1. [The CC proof
compiler](https://github.com/uwplse/potpie/tree/v0.4/Imp_LangTrick/ProofCompiler/ProofCompCodeCompAgnosticMod.v#L33)
compiler](Imp_LangTrick.ProofCompiler.ProofCompCodeCompAgnosticMod.html#CompilerAgnosticProofCompilerType.proof_compiler)
2. [The Tree proof compiler](https://github.com/uwplse/potpie/tree/v0.4/Imp_LangTrick/ProofCompiler/TreeProofCompiler.v#L15)
3. [The "preserves stack" relation, `exp_stack_pure_rel`](https://github.com/uwplse/potpie/tree/v0.4/Imp_LangTrick/Stack/StackPurestBase.v#L27)
4. [The relation between Imp environments and Stack's stacks](https://github.com/uwplse/potpie/tree/v0.4/Imp_LangTrick/SpecCompiler/LogicTranslationBase.v#L4)
Expand Down

0 comments on commit 34e5d7c

Please sign in to comment.