Int operations complexity

Stream: lean4

[Adrien Champion]

I'm in the process of writing a docstring for Init.Data.Int.Basic. Ideally I would like to discuss the complexity of the different operations, but it seems that's a technical question.

[Adrien Champion]

My understanding is that it depends on whether GMP is available or not; and if it is, it's not clear which algorithm is going to run in practice

[Adrien Champion]

Can anyone help on this matter? Discussions on specific operations, strategies for assessing asymptotic complexity, or links related to the topic would help a great deal

[Adrien Champion]

FYI, here is the PR on Int's docstring, without any real discussion on complexity:

• https://github.com/leanprover/lean4/pull/2167