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