Ssreflect Users Discussion List

[Épiphanie Gédéon <>]

You're right, it worked perfectly!

I understand coercions better now, a bit like in Haskell, you can only do first-type specifications

Le 16/02/2018 à 16:50, Jason Gross a écrit :

I believe

Coercion string_to_seq : string >-> seq.

Also works.  That is, coercion signatures take the head of the type.

- Jason

On Fri, Feb 16, 2018, 8:17 AM Épiphanie Gédéon <> wrote:

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"].