I'm reading a tutorial on Coq. It constructs a bool type as follows:

Coq < Inductive bool :  Set := true | false.
bool is defined
bool_rect is defined
bool_ind is defined
bool_rec is defined

Then it shows what each of these things are using "Check".

Coq < Check bool_ind.
bool_ind
     : forall P : bool -> Prop, P true -> P false -> forall b : bool, P b

Coq < Check bool_rec.
bool_rec
     : forall P : bool -> Set, P true -> P false -> forall b : bool, P b

Coq < Check bool_rect.
bool_rect
     : forall P : bool -> Type, P true -> P false -> forall b : bool, P b

I understand bool_ind. It says that if something holds for true and it holds for false, then it holds for all b in bool (because those are the only two).

But I don't understand what the expressions for bool_rec or bool_rect mean. It seems as if P true (which is a Set for bool_rec and a Type for bool_rect) is being treated as a propositional value. What am I missing here?

Edit
Report