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: Oct 13 2024 at 01:02 UTC