Ssreflect Users Discussion List

[Épiphanie Gédéon <>]

Oh I did not know this notation, I thought Coercions were supposed to 
have explicit types! So since I couldn't type (string >-> (seq ascii)), 
I thought wrappers were mandatory for it

Thank you a lot, I will use that instead


Le 16/02/2018 à 10:21, Laurent Thery a écrit :
> On 02/14/2018 02:08 AM, Épiphanie Gédéon wrote:
> > Hello all,
> >
> > I was wondering wether it was possible to coerce strings to a sequence
> > of ascii characters. Right now, I have been able to write this:
> >
> > Definition seq_string := seq ascii.
> >
> > Fixpoint string_to_seq_string (s: string): seq_string := match s with
> > |EmptyString => [::]
> > |String a s => a :: (string_to_seq_string s)
> > end.
> >
> > Coercion string_to_seq_string : string >-> seq_string.
> >
> > However, I am still unable to do this (with test a function over ascii):
> >
> > (map test "Hello")
> >
> > I have to do this:
> >
> > (map test ("Hello": seq_string))
> I am not an expert with coercion but the fact you have introduced an
> intermediate type seq_string may be the problem.
>
> This more direct way of encoding your coercion seems to work:
>
>  From mathcomp Require Import all_ssreflect.
> Require Import Ascii String.
>
> Fixpoint string_to_seq_string (s: string): seq ascii := match s with
> |EmptyString => [::]
> |String a s => a :: (string_to_seq_string s)
> end.
>
> Coercion string_to_seq := string_to_seq_string.
>
> Definition test : ascii -> ascii := id.
>
> Open Scope string_scope.
>
> Check [seq test i | i <- "Hello"].