Stream: Coq users

Topic: import ssreflect eqtype from coq


view this post on Zulip Andrey Klaus (Mar 31 2021 at 07:48):

Hello everyone!

quick question: what should I import to import eqtype from ssreflect ?

view this post on Zulip Andrey Klaus (Mar 31 2021 at 07:50):

here https://github.com/ilyasergey/pnp/blob/master/solutions/Rewriting_solutions.v

view this post on Zulip Andrey Klaus (Mar 31 2021 at 07:51):

author imports from mathcomp

view this post on Zulip Andrey Klaus (Mar 31 2021 at 07:52):

I do next according ssreflect manual:
From Coq Require Import ssreflect ssrfun ssrbool

view this post on Zulip Andrey Klaus (Mar 31 2021 at 07:52):

so, question, can I import eqtype from somewhere from Coq or should I use mathcomp ?

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 08:10):

You do need mathcomp

view this post on Zulip Andrey Klaus (Mar 31 2021 at 08:11):

thank you, I will install it then


Last updated: Feb 09 2023 at 00:03 UTC