• Dmitry Khalanskiy's avatar
    Add a stronger version of `list_core_id`. · d6dbed9e
    Dmitry Khalanskiy authored
    A new lemma, `list_core_id'`, allows to infer that a list is
    `CoreId` by only checking that all its elements are `CoreId`, as
    opposed to the existing instance, `list_core_id`, that only works
    when the list contains elements of the type where every element is
    `CoreId`.
    d6dbed9e
Name
Last commit
Last update
.gitlab/issue_templates Loading commit data...
benchmark Loading commit data...
docs Loading commit data...
tests Loading commit data...
tex Loading commit data...
theories Loading commit data...
.gitattributes Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
.gitmodules Loading commit data...
CHANGELOG.md Loading commit data...
CONTRIBUTING.md Loading commit data...
LICENSE Loading commit data...
LICENSE-CODE Loading commit data...
LICENSE-DOCS Loading commit data...
Makefile Loading commit data...
Makefile.coq.local Loading commit data...
ProofMode.md Loading commit data...
README.md Loading commit data...
_CoqProject Loading commit data...
build-all Loading commit data...
opam Loading commit data...
test-normalizer.sed Loading commit data...