Stream: Coq users

Topic: rec and rect

Julin S (Mar 12 2023 at 07:38):

When we define an inductive type, rec,rect,ind and 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?

Julin S (Mar 12 2023 at 07:39):

Was just looking for use cases where rec is needed.

Julin S (Mar 12 2023 at 07:39):

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
*)

Julin S (Mar 12 2023 at 07:39):

The type of P is the only thing that differs between ind, sind, rec and rect, right?

Julin S (Mar 12 2023 at 07:40):

Or is that only in the case of not-so-complex types?

Gaëtan Gilbert (Mar 12 2023 at 09:15):

with -impredicative-set it's possible to define types that have _rec but not _rect

Last updated: Oct 13 2024 at 01:02 UTC