Support typed atomic load and store #713
Annotations
1 error and 4 warnings
|
Run coq-community/docker-coq-action@v1:
new/proof/sync/atomic.v#L23
Tactic failure: iApply: cannot apply (▷ (addr ↦{dq} v -∗ ?Goal0 (# v)) -∗ WP ! (# addr) {{ v, ?Goal0 v }})%I.
|
|
Run coq-community/docker-coq-action@v1:
src/Helpers/ByteString.v#L44
IndW8 was already mapped to w8, mapping it also to @Naive.rep might yield ill typed terms when using the notation.
|
|
Run coq-community/docker-coq-action@v1:
src/Helpers/ByteString.v#L44
Type of IW8 seems incompatible with the type of W8. Expected type is: (Z → IndW8) instead of (Z → IndW8). This might yield ill typed terms when using the notation.
|
|
Run coq-community/docker-coq-action@v1:
src/Helpers/ByteString.v#L65
IndByteString was already mapped to byte_string, mapping it also to list might yield ill typed terms when using the notation.
|
|
Run coq-community/docker-coq-action@v1:
src/Helpers/ByteString.v#L65
Type of IByteString seems incompatible with the type of id_byte_string. Expected type is: (IndByteString → IndByteString) instead of (list → IndByteString). This might yield ill typed terms when using the notation.
|
Loading