I've very recently started learning Coq. I can't find the standard library code on GitHub. For example there is this : https://coq.inria.fr/library/Coq.Logic.FunctionalExtensionality.html
But it isn't a .v file or anything. It's a mere rendering (and maybe not complete/uptodate - and in any case I would like to see the real code). I thought it would be here:
But it isn't.
So I thought it was installed externally, via this:
But I can't find what I'm looking for. So I'm obviously doing something dumb. Please help!
I think the library you are looking for is located here:
inside coq's source code
Thanks. And in particular this:
"theories" huh? OK. I can get used to that!
It's not just the standard library that uses this terminology. You will find that many Coq packages have a
theories/ directory as well. And when there is a
src/ directory and a
theory/ directory, it usually means that this is a plugin and the OCaml code is in
Got it. And I should use the same.
I'm uncomfortable about the use of 'Axiom' in https://github.com/coq/coq/blob/master/theories/Logic/FunctionalExtensionality.v, much as I will probably use it. But how do you know you haven't imported a (non-Core) Axiom you don't want, or don't even know about? Or, more subtly, have imported (Require'd!) some code or a proof that uses such an Axiom somewhere deep inside? I mean, you don't want to have to look through imported files and all dependencies to make sure you haven't added Axioms unconsciously, right?
if you use
coq_makefile to generate your Makefile as in coq-mmaps, you can run
make validate and see what axioms you're using. If the axioms you use are defined in
Coq.Logic, you're fine w.r.t. consistency (to the best of what people currently know)
see section 4.1 in this document for advice on how to think about axioms and hypotheses in Coq
You can also
Print Assumptions lemma_name. to see which axioms were needed for that particular lemma
Last updated: Oct 01 2023 at 19:01 UTC