H: a<b
goal : a<?b=true
Why i cannot apply H directly?
The goal and H
have different types. You can use Nat.ltb_lt
.
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.
(a<?b) : bool : Type
H : (a<b) : Prop
goal : (a<?b = true) : Prop
Nat.lt_ltb is also possible?
Doesn't that do the opposite conversion?
Nat.ltb_lt
is an equivalence. You may use it in both directions. There is no lt_ltb
lemma.
Ok,thanks.
Last updated: Oct 13 2024 at 01:02 UTC