Thank you auggierose. Your comment is by far the best description of the stage of Litex is now: very flawed, but very different from other formal languages. I guess it is because Litex is closer to reasoning (or math in general) rather than to programming.

haha, no, it is not. visit my git commits and you can see the readme has been updated ~1000 times! I really want my readme look good!

Working on that bro :)

Thank you aktuel!

know @self_defined_axiom_larger_equal_is_transitive(x, y, z R): x >= y y >= z =>: x >= z

Since transitivity of >= is not implemented, one has to call this self_defined_axiom_larger_equal_is_transitive to make x >= 17 here, so

``` know forall x N: x >= 47 => x >= 17 ```

is essential

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.

HAHA, thank you fallat, I guess you are right!

have is used to ensure the existence of the object you define. For example, you do not want to declare a new object when it is from an empty set!

haha, you are right bro!

Thank you captain! Your observation is pretty interesting! I will fix that after I have more information!