Stream: Coq users

Topic: Is there way to use lia with ssreflect?


view this post on Zulip walker (Oct 19 2022 at 22:17):

So far eqP and friends are amazing when I have to do them once or twice (usually for f_equal)

But I am in a situation where I have list of hypothesis that are all using ssrnat, and goal that is in the same way. I know lia can solve it, but I was looking for a nice way to do it (or if ssreflect has alternative to lia that will automatically solve all nat goals).

view this post on Zulip Paolo Giarrusso (Oct 20 2022 at 01:30):

I think https://github.com/math-comp/mczify was the most recent effort for this? (The math-comp stream might have better answers)


Last updated: Jan 29 2023 at 05:03 UTC