Andrey Klaus (Mar 31 2021 at 07:48): Andrey Klaus (Mar 31 2021 at 07:48):Hello everyone!
quick question: what should I import to import eqtype from ssreflect ?
Andrey Klaus (Mar 31 2021 at 07:50):here https://github.com/ilyasergey/pnp/blob/master/solutions/Rewriting_solutions.v
Andrey Klaus (Mar 31 2021 at 07:51):author imports from mathcomp
Andrey Klaus (Mar 31 2021 at 07:52):I do next according ssreflect manual:
From Coq Require Import ssreflect ssrfun ssrbool
Andrey Klaus (Mar 31 2021 at 07:52):so, question, can I import eqtype from somewhere from Coq or should I use mathcomp ?
Matthieu Sozeau (Mar 31 2021 at 08:10):You do need mathcomp
Andrey Klaus (Mar 31 2021 at 08:11):thank you, I will install it then
Last updated: Oct 03 2023 at 04:02 UTC