Documentation

PrimeCert.Meta.SmallPrime

The small certificate method #

Looks up a pre-existing PrimeCert.prime_<n> declaration (from SmallPrimes.lean), e.g. PrimeCert.prime_31. Used as a base case in certificate ladders.

source
def PrimeCert.Meta.small_spec :
Lean.ParserDescr

Syntax for the small method: just a numeric literal n. Looks up the declaration PrimeCert.prime_<n> in the environment.

-- In a prime_cert% call:
prime_cert% [small {2; 3; 5; 7}, ...]
-- Each number must have a corresponding `PrimeCert.prime_<n>` theorem.
Equations
Instances For
    source
    def PrimeCert.Meta.mkSmallProof :
    PrimeCertMethod `PrimeCert.Meta.small_spec
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def PrimeCert.Meta.PrimeCertExt.small :
      PrimeCertExt
      Equations
      Instances For
        source
        def «step_groupSmall{_;}» :
        Lean.ParserDescr
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def step_groupSmall_ :
          Lean.ParserDescr
          Equations
          Instances For