Stream: Coq users

Topic: writing error ?

view this post on Zulip sara lee (Aug 25 2022 at 15:50):

I have different inductive types, want to remove error in following statement

Inductive loc: Type :=
 | Loc (a b: nat).

Inductive land: Type :=
 | Land  (lc:loc) (knd :kind).

Definition In_land (p: land) (pz :list land):=
  In (Loc p) (map Loc pz).

Last updated: Feb 04 2023 at 21:02 UTC