Stream: Coq users

Topic: selection of proper command


view this post on Zulip zohaze (Aug 11 2021 at 17:49):

a : nat
l0 : a <= 0

goal: a <= 0
I am applying command rewrite (leb_correct _ _ l0),but it does not work.

view this post on Zulip Lessness (Aug 11 2021 at 18:08):

Try auto or maybe exact l0, because it seems that l0 and goal is the same.


Last updated: May 24 2024 at 22:02 UTC