If I have a module with a
Parameter T : Type and function
f : T -> string, is there a way to define something like
Coercion f : T >-> string?
(If I try that as-is, I get
Error: Cannot recognize T as a source class of f.)
please elaborate, this works:
Require Import Strings.String. Parameter T : Type. Parameter f : T -> string. Coercion f : T >-> string.
or minimize, rather :-)
My bad, sorry... I just realized that
T is actually an
ordType (from https://github.com/arthuraa/extructures/blob/master/theories/ord.v).
Coercion won't let
(Ord.sort T) be a source class... maybe I should manually
Let T' : Type := Ord.sort T. and instead define
f : T' -> string and
Coercion f : T' >-> string, or something like that.
you can, but probably not Let; also coercion matching is syntactic, so you need an identity coercion if you want to also handle Ord.sort T...
Subclass lets you add a definition and coercion (https://github.com/Blaisorblade/dot-iris/blob/master/theories/Dot/examples/hoas.v#L43 has an example and the manual describes it); I'm not sure in which direction the generated coercion is...
I suspect with SubClass T' := Ord.sort T. you'd get a coercion to T', which would chain with your f.
Indeed, https://coq.inria.fr/refman/addendum/implicit-coercions.html#coq:cmd.SubClass agrees.
Beware that coercions can be polymorphic, but only of type
forall args..., class1 args... -> class2 args..., with both classes having the same arguments (this is the uniform inheritance condition); identity coercions are an exception.
Thanks for all the details. It seems like dealing with the occasional explicit
f is the path of least resistance (especially because I'm not sure if changing the type of
f is worth the overhead) :-P
Last updated: Sep 26 2023 at 12:02 UTC