Stream: Coq users

Topic: Induction principle for non-uniform parameterized types


view this post on Zulip yiyuan-cao (Jul 22 2023 at 07:01):

Inductive tree' (X : Type) : Type :=
  | leaf' (x : X)
  | node' (t : tree (X * X)).
Check tree'_ind.
(* tree'_ind *)
(*      : forall (X : Type) (P : tree' X -> Prop), *)
(*        (forall x : X, P (leaf' X x)) -> (forall t : tree (X * X), P (node' X t)) -> forall t : tree' X, P t *)

What is the useful induction principle for such parameterized but not homogeneous inductive types?

view this post on Zulip Notification Bot (Jul 22 2023 at 07:19):

yiyuan-cao has marked this topic as unresolved.

view this post on Zulip Paolo Giarrusso (Jul 22 2023 at 11:24):

Should tree be tree'? Your given example is homogeneous


Last updated: Jun 13 2024 at 19:02 UTC