When we define an inductive type,
sind get made as well, right?
These are induction principles tailored for Set, Type, Prop and SProp, isn't it?
Why were seperate lemmas needed for Set and Type? Couldn't
rect stand in for
rec as well?
Was just looking for use cases where rec is needed.
Check nat_rec. (* nat_rec : forall P : nat -> Set, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n *) Check nat_rect. (* nat_rect : forall P : nat -> Type, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n *)
The type of P is the only thing that differs between ind, sind, rec and rect, right?
Or is that only in the case of not-so-complex types?
with -impredicative-set it's possible to define types that have _rec but not _rect
Last updated: Oct 04 2023 at 20:01 UTC