12
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?