Stream: Coq users

Topic: short form


view this post on Zulip zohaze (Oct 21 2022 at 17:35):

H: a<b
goal : a<?b=true

Why i cannot apply H directly?

view this post on Zulip Olivier Laurent (Oct 21 2022 at 17:55):

The goal and H have different types. You can use Nat.ltb_lt.

view this post on Zulip Pierre Courtieu (Oct 22 2022 at 09:41):

Let's add that you should be cautious not to take bool for Prop. To sum up, here are the typing relations. Note in particular that a<b is a type whereas a<?b is a value, and they don't live in the same sort.

view this post on Zulip zohaze (Oct 24 2022 at 14:15):

Nat.lt_ltb is also possible?

view this post on Zulip James Wood (Oct 24 2022 at 14:18):

Doesn't that do the opposite conversion?

view this post on Zulip Pierre Castéran (Oct 24 2022 at 15:05):

Nat.ltb_lt is an equivalence. You may use it in both directions. There is no lt_ltb lemma.

view this post on Zulip zohaze (Oct 25 2022 at 04:38):

Ok,thanks.


Last updated: Oct 13 2024 at 01:02 UTC