Better soundness lemma & cleanup
- Define refines_sound and use it in all the examples. - Rename lty_ → lrel_
Showing
- theories/examples/bit.v 3 additions, 26 deletionstheories/examples/bit.v
- theories/examples/generative.v 23 additions, 8 deletionstheories/examples/generative.v
- theories/examples/or.v 2 additions, 2 deletionstheories/examples/or.v
- theories/examples/symbol.v 35 additions, 24 deletionstheories/examples/symbol.v
- theories/examples/ticket_lock.v 17 additions, 1 deletiontheories/examples/ticket_lock.v
- theories/lib/Y.v 1 addition, 1 deletiontheories/lib/Y.v
- theories/lib/assert.v 1 addition, 3 deletionstheories/lib/assert.v
- theories/lib/counter.v 3 additions, 6 deletionstheories/lib/counter.v
- theories/lib/list.v 11 additions, 11 deletionstheories/lib/list.v
- theories/lib/lock.v 2 additions, 2 deletionstheories/lib/lock.v
- theories/logic/model.v 10 additions, 10 deletionstheories/logic/model.v
- theories/prelude/bijections.v 9 additions, 6 deletionstheories/prelude/bijections.v
- theories/typing/fundamental.v 2 additions, 2 deletionstheories/typing/fundamental.v
- theories/typing/soundness.v 12 additions, 0 deletionstheories/typing/soundness.v
Loading
Please register or sign in to comment