The first line is essential, because Litex does not implement transitivity of >= in its kernel and one has to formalize it:
know @larger_equal_is_transitive(x, y, z R):
x >= y
y >= z
Thank you for clarifying, but don't you think this puts a rather big dent in the claim that Litex is "intuitive" and "can be learned by anyone in 1–2 hours"? I think the average user would expect the natural/real numbers to come equipped with this kind of theorems.
For instance, the tutorial says that "The daily properties" (whatever this means) of "+, -, , /, ^, %" are "already in the Litex kernel". What about associativity of and +, or distribution of * over +? Are these part of the "daily properties"? And if so, why didn't transitivity of >= not make the cut?
Just trying to understand the design choices here, this is very interesting.
lou1306|5 months ago
For instance, the tutorial says that "The daily properties" (whatever this means) of "+, -, , /, ^, %" are "already in the Litex kernel". What about associativity of and +, or distribution of * over +? Are these part of the "daily properties"? And if so, why didn't transitivity of >= not make the cut?
Just trying to understand the design choices here, this is very interesting.