Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
100-theorems
Arithmetic
Lispfloat
Arithmetic-1
Number-theory
Tonelli-shanks-modular-sqrt-algorithm
Tonelli-shanks-algorithm-is-correct
Tonelli-shanks-even-sqrt
Tonelli-shanks-odd-sqrt
Tonelli-shanks-lesser-sqrt
Tonelli-shanks-greater-sqrt
Tonelli-shanks-sqrt
Tonelli-shanks-either-sqrt
Tonelli-shanks-supportive-functions
Repeated-square
Q*2^s
Defprime
Defprime-alias
Dm::primep
Prime
Has-square-root?
Prime-fix
Secp256k1-group-prime
Secp256k1-field-prime
Jubjub-subgroup-prime
Edwards-bls12-subgroup-prime
Bn-254-group-prime
Bls12-381-scalar-field-prime
Baby-jubjub-subgroup-prime
Goldilocks-prime
Proof-by-arith
Arith-equivs
Include-an-arithmetic-book
Number-theory
Arithmetic-3
Arithmetic-2
Arithmetic-light
Arithmetic-5
Bit-vectors
Algebra
Testing-utilities
Tonelli-shanks-modular-sqrt-algorithm
Tonelli-shanks-supportive-functions
Supportive Functions
Supportive functions for the Tonelli-Shanks modular square root algorithm
Subtopics
Repeated-square
Q*2^s