CODEWITHSUNDEEP
coq
Shuheng Zheng
Shuheng Zheng

Reputation: 297

Curly brace in Coq generics

The following code gives an error:

Inductive mylist {A : Set} : Set :=
| mylist_Nil
| mylist_Cons : A -> mylist A -> mylist A.

The error is "mylist A" of type "Set" cannot be applied to the term "A" : "Set". If I change "{A:Set}" to (A:Set) then it works fine.

What does the curly braces mean? Thanks!

Upvotes: 6

Views: 697

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23582

Usually, arguments are declared using parentheses. Curly braces are used for implicit arguments. Implicit arguments are not passed to functions and type declarations like usual ones; instead, the Coq type-checker tries to figure out what they should be from the context.

You can force a constant to take all arguments explicitly with an @ sign, like this: @mylist A.

For generic types like mylist, there isn't enough context for Coq to infer what the A parameter should be, so it is usually better to declare those parameters explicitly, with parentheses.

The Coq user manual has more information on implicit arguments.

Upvotes: 9

Related Questions