I have an inductive type that looks like
Inductive A : Type := | Abase : A | Alist : list A -> A .
I'd like to use
Alist as a coercion, how can I achieve that?
Definition isA : A := (nil : list A).
I don't know a way to do exactly that, but here is something close. Feel free to ask questions.
Inductive A : Type := | Abase : A | Alist : list A -> A . Module Import test. Definition listA := list A. Identity Coercion Id_listA_list : listA >-> list. #[global] Arguments Id_listA_list /. Coercion Alist' := Alist : listA -> A. #[global] Arguments Alist' /. End test. Definition isA : A := (nil : listA).
Note the coercion applies to
list A; coercions (like much else in Coq) distinguish between definitionally equal but syntactically different terms.
what's the identity coercion for?
good point; I was trying to get bidirectional coercions between
list A and
listA, but then I remembered I never got that to work because of the uniform inheritance condition.
That seems disappointing, since working around that restriction is a crucial use-case for identity coercions.
Indeed, I rechecked https://coq.inria.fr/refman/addendum/implicit-coercions.html#identity-coercions and the same question applies.
Maybe you’re supposed to replace all uses of
list A with
listA by hand in your development? That’s what I did other times.
Matthis Kruse has marked this topic as resolved.
Last updated: Jan 27 2023 at 01:03 UTC