ProblemExtraction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Special commands to aid in "problem extraction".

For the math problems that we archive, we aim to include proofs in-line. Sometimes, however, we want to present the problems without giving away information about the solutions. Therefore, we have "problem extraction" -- a means of stripping solutions.

During problem extraction, all declarations are removed except those that have been tagged with one of the below command wrappers.

Imports (1)
Imported by 525 files
  1. def ProblemExtraction.elabProblemFile line 29 source

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

    Statement uses: Lean.Syntax, Option, Lean.TSyntax, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, Lean.Elab.Command.CommandElabM, Unit

    Proof uses: String.Pos.Raw, Lean.Syntax.getTailPos?, Lean.TSyntax.raw, Bool.false, Bind.bind, Lean.Elab.Command.Context, MonadReader.read, StateRefT', IO.RealWorld, Lean.Elab.Command.State, EIO, Lean.Exception, String, Lean.FileMap.source, Lean.Elab.Command.Context.fileMap, String.Pos.Raw.mk, HAdd.hAdd, Nat, String.Pos.Raw.byteIdx, OfNat.ofNat and 43 more

    21 instances, coercions and auxiliary constants left out.