how does tactic.ring work?

Stream: maths

[Johan Commelin]

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

[Johan Commelin]

It computes in binary instead of unary arithmetic.

[Kevin Buzzard]

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]

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