Use list based environment representation.
This eases proofs, because lists computes. It also avoids issues with duplicates (so, no more environment splitting judgment, just append).
Showing
- theories/logrel/environments.v 155 additions, 148 deletionstheories/logrel/environments.v
- theories/logrel/examples/double.v 2 additions, 3 deletionstheories/logrel/examples/double.v
- theories/logrel/examples/mapper.v 22 additions, 27 deletionstheories/logrel/examples/mapper.v
- theories/logrel/examples/pair.v 7 additions, 15 deletionstheories/logrel/examples/pair.v
- theories/logrel/lib/mutex.v 24 additions, 42 deletionstheories/logrel/lib/mutex.v
- theories/logrel/lib/par_start.v 20 additions, 45 deletionstheories/logrel/lib/par_start.v
- theories/logrel/term_typing_judgment.v 27 additions, 7 deletionstheories/logrel/term_typing_judgment.v
- theories/logrel/term_typing_rules.v 203 additions, 271 deletionstheories/logrel/term_typing_rules.v
Loading
Please register or sign in to comment