FormalConjecturesUtil/Attributes/AMS.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

AMS Subject classification

This file defines some tools used by the ProblemSubject attribute in order classify problems by their corresponding AMS Subject.

The AMSDescription has one term for each number n ∈ {1, ..., 96} that has a corresponding AMS subject, namely AMSDescription.«n». Note that not all values of n in this interval are assigned a subject.

To extract the value corresponding to n, one can use numToAMSDescriptions n. This is useful for getting the doctring that corresponds to the subject n when parsing the attribute.

Finally, to access the list of subjects and their corresponding number when editing Lean files, we implement a #AMS command that prints this list.

Imports (3)
Imported by 1 file
  1. inductive AMS line 44 source

    no axioms what this means

  2. def AMS.getDesc line 178 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: AMS, Lean.Core.CoreM, String

    Proof uses: Lean.Expr, Lean.ToExpr.toExpr, Lean.Name, Bind.bind, Lean.Environment, Lean.MonadEnv.getEnv, Option, liftM, EIO, IO.Error, ReaderT, Lean.Core.Context, StateRefT', IO.RealWorld, Lean.Core.State, Lean.Exception, IO, Lean.findDocString?, Bool.true, EmptyCollection.emptyCollection and 13 more

    23 instances, coercions and auxiliary constants left out.

  3. def AMS.toNat? line 183 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: AMS, Option, Nat

    Proof uses: Lean.Expr, Lean.ToExpr.toExpr, Lean.Name, String, String.toNat?, Option.none

    2 instances, coercions and auxiliary constants left out.