qed auditor checkUpd #615
Annotations
5 warnings
|
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
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