zohaze (Aug 30 2022 at 16:50): zohaze (Aug 30 2022 at 16:50):I am proving , a <=? b = true (forall a b :nat). I am destructing leb, but i get message " Use Bool.le ". When i use this then again get error .
James Wood (Aug 31 2022 at 11:01):Do you mean to say that you have an assumption of the form (a <=? b) = true? Indeed, such an assumption is likely to be difficult to work with as-is, and you may want to convert it into an a <= b by applying leb_complete. Alternatively, you could make the leb (<=?) compute by destructing a and b, following the pattern-matching in the definition of leb.
Last updated: Apr 19 2024 at 09:01 UTC