Stream: math-comp users

Topic: \max in order.v


view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2021 at 09:50):

Hi folks, I was wondering how to use the \max notations that are reserved in order.v ; they are there, however I'm not sure they are actually implemented, right? cc: @Cyril Cohen

view this post on Zulip Cyril Cohen (Oct 01 2021 at 12:17):

Emilio Jesús Gallego Arias said:

Hi folks, I was wondering how to use the \max notations that are reserved in order.v ; they are there, however I'm not sure they are actually implemented, right? cc: Cyril Cohen

Looks like you are right

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2021 at 15:11):

@Cyril Cohen you wanna me open a bug upstream? [I may even submit a PR would I have time, tho I wonder how to handle orders without \bot]


Last updated: Mar 28 2024 at 09:01 UTC