There are a few already defined propositions: Just like types, propositions can be defined inductively using the Inductive command. Here is how one could define the length of a list as a recursive function:įixpoint length (xs: list A): list A := rev_acc xs nil. To build a recursive function, one must use a different command than Definition, namely Fixpoint. The Definition command that we have used so far is quite restrictive in the sense that it does not allow for recursion. If you wish to be able to explicitly pass arguments to implicit parameters, simply add an before the name of the definition: Once this is done, we can build lists without explicitly passing the type argument. To declare the type parameter A of the two constructors as implicit, we can use the following commands:
Therefore, if we were, for instance, to build a list containing the bools true and false, we would have to explicitly pass the type parameter bools to all constructors.Ĭheck (cons bool true (cons bool false (nil bool))).Ĭoq however support implicit parameters. If you check the type of nil and of cons, you will see that they have as a first argument the type A. We write list A for a list of elements of type A. Notice that list takes a type parameter A. For instance, here is a definition of generic lists in Coq: We can also define inductive data types in Coq. The result (which is true : bool) should appear in a panel of your IDE. Simply type and interpret the following command to see the type of true: To check the type of an expression, you may find useful to use the Check command. Your IDE should have a button / command to interpret forward by one command, or to interpret to the current cursor. Important note: If you are following along in your IDE (which we highly suggest you do), be sure to interpret commands as we go along. Each command in Coq is ended by a single point.
Note the point at the end of the definition. The name of the type defined here is bool, and the type as two constructors: true and false.
In Coq, we can define algebraic datatypes using the Inductive construct.įor instance, to define booleans, one simply needs to write:
Coq definition how to#
First, we will see how to define datatypes.
0 kommentar(er)
