This page gives a (very) short description of a branch of the development of Coq, called Coq*. This prototype is based on Bruno Bernardo's Ph.D. work, and is developed by Bruno Barras.
The theory behind this prototype is based on Miquel's Implicit Calculus of Constructions (ICC). It allows the user to use 2 kinds of products:forall x:A,B
(or A->B
)forall [x:A],B
(or [A]->B
)Inductive obj : Type := repr : forall [A:Type], A -> obj.
It is available as a darcs repository.
You can get a working copy with the following command:
darcs get http://www.lix.polytechnique.fr/Labo/Bruno.Barras/darcs/V8-implicit/
If you don't use darcs, you can simply recursively download folder
http://www.lix.polytechnique.fr/Labo/Bruno.Barras/darcs/V8-implicit/_darcs/pristine/
.
Note about versions: Coq* tries to follow the development of Coq as closely as possible. Currently, the above code is based on SVN revision 10047 of the development trunk of coq.
It compiles in the same way as Coq:
./configure [...config options...]
make
make install
This command builds the same executables as Coq (coqtop, coqc and coqide), both bytecode and native versions.
Basically, the usage is the same as Coq. You are just allowed to put [ ] around bindings to declare implicit arguments. It is not mandatory to tag implicit arguments passed to functions, the typechecker infers that automatically. See the examples below to get the idea.
There is just one new vernacular command to print the extracted term (in the sense of ICC):
Print Extraction <term>.
Some tactics have been extended to support for implicit arguments.
generalize [ <constr> ]
introduces an implicit
product instead of an explicit one