Lean2Js.Sha256
SHA-256 #
SHA-256, so that a package can carry the digest of every file it ships beside the theorems it ships.
The digest is the plain one shasum -a 256 prints. A consumer checking that the index.js in front of
them is the one the manifest speaks about has neither Lean nor this compiler, so the check has to be one
their own machine already knows how to do.
The three vectors below are FIPS 180-4's own. They are what says the table of constants was copied correctly: every one of them is wrong the moment a digit is.
Lean2Js.Sha256.hash
sourceEquations
- One or more equations did not get rendered due to their size.
Instances For
Used by
Lean2Js.Sha256.hex
sourceEquations
- One or more equations did not get rendered due to their size.
Instances For
Used by
Lean2Js.Sha256.digest
sourceThe digest of a file's bytes, spelled the way shasum -a 256 spells it.