CODEWITHSUNDEEP
coq
thor
thor

Reputation: 22460

What's the square bracket syntax [ |- Set] in Coq?

I some times see this syntax in Coq to represent certain types/sets such as in printing information about existential variables:

?T : [ |- Set]
?T0 : [ x : ?T |- Set ]

I don't know how to search for this syntax.

What does it mean?

Is the first one the same as 

? T : Set

?

Upvotes: 3

Views: 632

Answers (2)

larsr
larsr

Reputation: 5811

Suppose we have a term with a certain type.

Variable B : nat -> nat.
Check B.
(*
B
     : nat -> nat
 *)

If we create another term using B it may or may not type check, i.e. B true is not typeable. 

Fail Check B true.
(*
 Error message:
 The term "true" has type "bool" while it is expected to have type "nat".
 *)

Coq allows wildcards in terms and then tries to figure out the type itself.

Check B _.
(*
B ?n
     : nat
where
?n : [ |- nat]
 *)

Here Coq says that the type of B _ is nat, but only under the assumption that the argument (named ?n) is of type nat. Or otherwise put, "under the assumption that one can infer that the type of ?n is nat from the empty context".

Sometimes more stuff is found on the left side of the "turnstile" symbol |-.

Variable x:nat.
Check _ x.
(*
?y x
     : ?T@{x:=x}
where
?y : [ |- forall x : nat, ?T] 
?T : [x : nat |- Type] 
*)

Above the underscore is called ?y and the type of (?y x) is a dependent type ?T that depends on x. ?T is only typable (to a Type) in a context where x is a nat. If x is not a nat, then ?T is not typable.

Upvotes: 5

Vinz
Vinz

Reputation: 6047

I might be mistaken, but the first one should be read as "the existential variable named T is of type Set" and the second should be read as "the existential variable named T0 is of type Set, in a context where the variable x is of type ?T", meaning that the term which will fill the second hole might depend on some variable named x.

Upvotes: 0

Related Questions