Sometimes the "class" command can be rather slow, for example: class archimedean_field = ordered_field + assumes ex_less_of_nat: "EX n. x < of_nat n"
### command "class" ### User 2.596 All 2.604 secs For comparison, deriving from earlier classes is a lot faster: class archimedean_field = semiring_1 + ord + assumes ex_less_of_nat: "EX n. x < of_nat n" ### command "class" ### User 0.272 All 0.272 secs And finally, a temptation to just give up and use "axclass": axclass archimedean_field < ordered_field ex_less_of_nat: "EX n. x < of_nat n" ### command "axclass" ### User 0.008 All 0.008 secs I don't know what the "class" command is doing behind the scenes, but is it supposed to be taking this long? Should this be considered a performance bug? - Brian
