def EvalAuto.Environment.newLocalConstants (env₁ env₂ : Lean.Environment) : Array Lean.ConstantInfo

Suppose env₂ is the environment after running several non-import commands starting from env₁, then Environment.newLocalConstants env₁ env₂ returns the new ConstantInfos added by these commands

Equations

• One or more equations did not get rendered due to their size.

def EvalAuto.mathlibModules : Lean.CoreM (Array Lean.Name)

Equations

• One or more equations did not get rendered due to their size.

def EvalAuto.allMathlibModuleNamesCanBeFilename : Lean.CoreM Bool

Equations

• EvalAuto.allMathlibModuleNamesCanBeFilename = do let mms ← EvalAuto.mathlibModules pure (mms.all EvalAuto.Name.canBeFilename)

def EvalAuto.Array.randPick {α : Type} (xs : Array α) (n : Nat) : IO (Array α)

Pick n elements from array xs. Elements may duplicate

Equations

• One or more equations did not get rendered due to their size.

def EvalAuto.Array.randPickNodup {α : Type} (xs : Array α) (n : Nat) : IO (Array α)

Equations

• One or more equations did not get rendered due to their size.

def EvalAuto.Array.pseudoRandPickNodup {α : Type} (xs : Array α) (n : Nat) (gen : StdGen) : Array α × StdGen

Equations

• One or more equations did not get rendered due to their size.