Skip to content
Snippets Groups Projects
Commit c4ece0aa authored by Michael Sammler's avatar Michael Sammler
Browse files

start with GUIDE

parent ef26b9b0
No related branches found
No related tags found
No related merge requests found
GUIDE.md 0 → 100644
# WIP: Guide for RefinedC developers
This guide has two parts: First, a guide for writing typing rules.
Second, a style guide for RefinedC development.
## Rule guide
1. `SimplifyHyp` and `SimplifyGoal` rules should match: The
information learned by the `SimplifyHyp` rule should be enough to
prove the `SimplifyGoal`. Said another way, applying the
`SimplifyHyp` instance and then proving `SimplifyGoal` should be
equivalent to not using any of the two (except for learning more
information).
## Style guide
1. Follow the std++/Iris style.
2. If there is a typeclass to restrict when a typing rule applies, but
it does not contain useful information for proving the typing rule,
it should only be on the instance, not the lemma.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment