Proper handling of the unboxed types
Prior to this change there was a bit of a mess in handling of types on which you can do `CAS` and which you can compare by equality. This change adds typing rules that allow `CAS` on any unboxed types.
Showing
- _CoqProject 2 additions, 0 deletions_CoqProject
- theories/logic/compatibility.v 65 additions, 0 deletionstheories/logic/compatibility.v
- theories/prelude/lang_facts.v 197 additions, 0 deletionstheories/prelude/lang_facts.v
- theories/typing/contextual_refinement.v 29 additions, 28 deletionstheories/typing/contextual_refinement.v
- theories/typing/contextual_refinement_alt.v 148 additions, 0 deletionstheories/typing/contextual_refinement_alt.v
- theories/typing/fundamental.v 33 additions, 21 deletionstheories/typing/fundamental.v
- theories/typing/interp.v 29 additions, 0 deletionstheories/typing/interp.v
- theories/typing/soundness.v 12 additions, 7 deletionstheories/typing/soundness.v
- theories/typing/types.v 16 additions, 10 deletionstheories/typing/types.v
Loading
Please register or sign in to comment