ssreflect - [ssreflect] Debugging canonicals

Subject: Ssreflect Users Discussion List

List archive

[ssreflect] Debugging canonicals

From: Florent Hivert <>
To: "" <>
Subject: [ssreflect] Debugging canonicals
Date: Mon, 16 Dec 2019 20:09:57 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=Pass ; spf=None
Ironport-phdr: 9a23:5I20QxYNsyygJFGiHCvAAIb/LSx+4OfEezUN459isYplN5qZoMS/bnLW6fgltlLVR4KTs6sC17ON9fq4BCdZu87JmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRu7oR/PusUKgYZuJbs9xgXVrnBVZ+lY2GRkKE6JkR3h/Mmw5plj8ypRu/Il6cFNVLjxcro7Q7JFEjkoKng568L3uxbNSwuP/WYcXX4NkhVUGQjF7Qr1UYn3vyDnq+dywiiaPcnxTbApRTSv6rpgRRH0hCsbMTMy7WfagdFygq1GuhKsvxJxzY7Kbo+IN/Rxcb/Scs4USmdaQsZdSzBNDp+gY4YVEeYMO/tToYnnp1sJqBuzHQmiBOfoyj9SmHD227E62PkjHwHHwgwvAcgOsGjJp9jyNKkSVee1zLPWwjXFc/NawzXz6InWch8/u/GMQal9cc7LyUkuDQ/FgE+QpJXjMjiI2OoNtG2b4PBhVeKpk2MnrwBxoj6xycg2kInFnIcVxUrc9Sh/3Y07JsW4RVZmbdK6FJZcrTyWOol2T884Xm1luDw2xqAatZO9YSME0o4oxwTFZPyCa4WI4gzsVOKWITpggXJqYrO/hxKs/kmv1u3wTM200ExLriZfnNnMrGgB1x3V6seZVvtw5lqt1SiL2gzJ9+1JI0A5mbDGJ5Mh2LI8i4YfvVzGHiDsmUX2iKGWdl8j+uit8+npYrHmppiGN4BqjAH+Lr4ilM6+AeQmLAcORXSb9P+41L35/E31WrtKjucunqnDrJ/aPdgbprK+AwJNyYYj8Ay/ACmo0NQcg3YIME5FdQmcj4npPlHOOOr3Ae2+g1SqijdrxurJMqfvApXXfTD/l+KrZq1n5kBYxQEv5dVE/ddVDKsAKbTyXFXwvZrWFFVxZxev2evpDNh2yqsbQnjKA6mDMaqUsFmS5+tpLfPaN6EPvzOoBfwi/fPokTcZmEEQZ7XhibUTb2q1GOggA0SHbGDwqtMbECEEpFxtH6TRlFSeXGsLND6JVKUm62RjUd/0PcL4XomoxYe58mK7E5lRPz4UD1mNFXr4a8OAQfZKZjjAepY9wAxBbqCoTsoa7T/rrBXzm+hjNOuS9DdK7cuyhugw3PXakFQJzRIxCs2c12+XSGQkzGcSRnk4xvImrA==

Dear all,

In the following scenario, linearZ is not accepting an algebra morphisme
between two R-algebras. How is this possible ?

Florent

Variable R : comRingType.

Check fps_algType : algType R.
Check (tfps_algType R _) : algType R.

Let mor i : {lrmorphism fps_algType -> tfps_algType R i} :=
[lrmorphism of pi_phant (Phant {series R}) i].

Let bla2 i := linearZ (mor i).
Error:
In environment
R : comRingType
bla1 := fun i : nat_dirType => rmorph1 [lrmorphism of 'pi_i]
: forall i : nat_dirType, [lrmorphism of 'pi_i] 1 = 1
mor := fun i : nat => [lrmorphism of 'pi_i]
: forall i : nat, {lrmorphism fps_algType -> tfps_algType R i}
i : nat
The term "mor i" has type "{lrmorphism fps_algType -> tfps_algType R i}"
while it is expected to have type
"GRing.Linear.map_for ?U ?s ?a (GRing.Scale.op ?h_law ?c)".

[ssreflect] Debugging canonicals, Florent Hivert, 12/16/2019
- Re: [ssreflect] Debugging canonicals, Florent Hivert, 12/17/2019

List archive

[ssreflect] Debugging canonicals