Stream: Coq users

Topic: rec and rect


view this post on Zulip 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?

view this post on Zulip Julin S (Mar 12 2023 at 07:39):

Was just looking for use cases where rec is needed.

view this post on Zulip 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
*)

view this post on Zulip 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?

view this post on Zulip Julin S (Mar 12 2023 at 07:40):

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

view this post on Zulip 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: Jun 14 2024 at 19:02 UTC