2

Coq 8.7 integrates the popular Ssreflect library. Its libraries can hence be imported in the following manner:

From Coq Require Import ssreflect ssrfun ssrbool.

However, when I try to import ssrnat it complains that it's Unable to locate library ssrnat with prefix Coq, and I cannot find ssrnat in the Coq distribution on disk either. Was ssrnat deliberately not included for some reason, or folder into another module, or is there just something wrong with my installation?

3
  • 2
    Does From mathcomp Require Import ssrnat. work? Dec 16, 2017 at 9:51
  • That gives "Cannot find a physical path bound to logical path matching suffix <> and prefix mathcomp." (I don't have mathcomp installed. Should I?). Dec 16, 2017 at 9:56
  • Despite the fact the Coq Refman mentions ssrnat, it's not in the standard library as of now (my installation has only ssreflect, ssrfun, and ssrbool in $HOME/.opam/4.06.0/lib/coq/plugins/ssr directory). So, yes you should install mathcomp. Incidentally, this question might help with installation. Dec 16, 2017 at 10:29

1 Answer 1

4

ssrnat is not included in the main Coq distribution, although some day we hope to provide an extended distribution where more libraries are available by default.

In Coq 8.7, only the tactic language itself ssreflect plus a few basic supporting libraries ssrfun ssrbool were included.

The reason we didn't include more is because ssrnat makes use of the math-comp mathematical hierarchy so this is a more "invasive" change.

Fortunately, thanks to the plugin being included, installing ssrnat is a very easy task.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.