Stream: math-comp users

Topic: ✔ Converting Coq (normal) Field Type to math-comp fieldType

Notification Bot (May 21 2022 at 10:33):

Mukesh Tiwari has marked this topic as resolved.

Karl Palmskog (May 21 2022 at 11:32):

@Mukesh Tiwari I think the community would appreciate if you posted a link to your solution (e.g., use GitHub Gist)

Mukesh Tiwari (May 21 2022 at 12:09):

@Karl Palmskog It was simple but very informative. I followed this Rstruct.v from the FFS-CoqRK-FP. I used Coq.Logic.Epsilon to get the choiceType, same as the FFS-CoqRK-F library. Here is the gist, but it still has few admits because there is nothing in (normal) Field type about the interaction between 0 (rO) and * (rmul).

Last updated: Jan 29 2023 at 18:03 UTC