Stream: Coq users

Topic: error removal


view this post on Zulip 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 .

view this post on Zulip 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: Feb 01 2023 at 11:04 UTC