|
|
|---|
|
|
|
|---|
The constant
This is copied and pasted from [ZPS], and visually compared with it. Nonetheless, eventually it would be good to replicate, in ACL2, its calculation, which is described in [ZPS:5.9].
Definition:
(defconst *urs* (acl2::string=>nats "096b36a5804bfacef1691e173c366a47ff5ba84a44f26ddd7e8d9f79d5b42df0"))