## Stream: maths

### Topic: how does tactic.ring work?

#### Johan Commelin (Jun 13 2018 at 10:02):

@Kevin Buzzard Re 2: Because znum is a fast (but somewhat "unmathematical") implementation of int.

#### Johan Commelin (Jun 13 2018 at 10:02):

It computes in binary instead of unary arithmetic.

#### Kevin Buzzard (Jun 13 2018 at 10:03):

If that's the only reason then I might rip them out and replace them with ints because I am trying to de-obfuscate. I just don't want to rip them all out and then find that some meta code stops working!

#### Johan Commelin (Jun 13 2018 at 10:04):

Hmm, I can't change the stream... even though I changed the topic... [meeh]

Last updated: May 11 2021 at 00:31 UTC