CODEWITHSUNDEEP
coq
Greg Nisbet
Greg Nisbet

Reputation: 6994

Use coqtop to check type of expression

I'm curious about the type of the Coq entities equivalent to connectives in logic. For the sake of specificity, let's say -> and /\. If -> is a magical non-[first-class entity], then let's just use /\ as the entity. I'm curious whether its domain is Prop or Set.

Is it possible to use coqtop to get the type of an expression?

I want to do something similar to the following with ghci.

> ghci
:GHCi, version 8.6.3:  :? for help
Prelude> :t (**)
(**) :: Floating a => a -> a -> a

Upvotes: 1

Views: 463

Answers (1)

SCappella
SCappella

Reputation: 10424

/\ and -> are both notations, rather than actual constants in Coq. To find their signatures, you have to first determine what they are a notation for. Running the command Locate "/\". should output something along the lines of

Notation
"A /\ B" := and A B : type_scope
(default interpretation)

So /\ is a notation for the constant and. Then you can use the command Check to find its type. Check and. gives

and
     : Prop -> Prop -> Prop

So and takes two Props and gives a Prop.

Similarly, A -> B is a notation for forall _: A, B. Unlike and, forall isn't a constant, but rather a keyword in the language of Coq, so you can't use Check forall. to get the signature. In this case, you could look in the reference manual for products and see that

The expression forall ident : type, term denotes the product of the variable ident of type type, over the term term. As for abstractions, forall is followed by a binder list, and products over several variables are equivalent to an iteration of one-variable products. Note that term is intended to be a type.

So that means that both A and B should be types, which means they could be elements of any of the universes Prop, Set or Type.

Upvotes: 5

Related Questions