inductive Auto.LemDB : Type

Lemma database is a collection of lemmas that users can supply to a tactic. Users only need to provide the name of the lemma database to the tactic. Each lemma database has a name, which is internally stored as a Name. User can add a lemma to a lemma database (internally, .addLemma), or combine several existing lemma databases to form a larger lemma database (internally, .compose), or both. Note that .compose is dynamic.

• empty : LemDB
• addLemma (lem : Lean.Name) (lemdb : LemDB) : LemDB
• compose (lemdbs : Array Lean.Name) : LemDB

instance Auto.instBEqLemDB : BEq LemDB

Equations

• Auto.instBEqLemDB = { beq := Auto.beqLemDB✝ }

instance Auto.instHashableLemDB : Hashable LemDB

Equations

• Auto.instHashableLemDB = { hash := Auto.hashLemDB✝ }

instance Auto.instInhabitedLemDB : Inhabited LemDB

Equations

• Auto.instInhabitedLemDB = { default := Auto.LemDB.empty }

instance Auto.instReprLemDB : Repr LemDB

Equations

• Auto.instReprLemDB = { reprPrec := Auto.reprLemDB✝ }

@[reducible, inline]

abbrev Auto.LemDBExtension : Type

Equations

• Auto.LemDBExtension = Lean.PersistentEnvExtension (Lean.Name × Auto.LemDB) (Lean.Name × Auto.LemDB) (Std.HashMap Lean.Name Auto.LemDB)

opaque Auto.lemDBExt : LemDBExtension

partial def Auto.LemDB.toHashSet : LemDB → Lean.AttrM (Std.HashSet Lean.Name)

def Auto.registerAddLemToDB : IO Unit

Equations

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

def Auto.findLemDB (dbname : Lean.Name) : Lean.CoreM (Option LemDB)

Equations

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

def Auto.declarelemdb : Lean.ParserDescr

Equations

• Auto.declarelemdb = Lean.ParserDescr.node `Auto.declarelemdb 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#declare_lemdb") (Lean.ParserDescr.const `ident))

def Auto.printlemdb : Lean.ParserDescr

Equations

• Auto.printlemdb = Lean.ParserDescr.node `Auto.printlemdb 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#print_lemdb") (Lean.ParserDescr.const `ident))

def Auto.composelemdb : Lean.ParserDescr

Equations

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

def Auto.elabdeclarelemdb : Lean.Elab.Command.CommandElab

Equations

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

def Auto.elabprintlemdb : Lean.Elab.Command.CommandElab

Equations

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

def Auto.elabcomposelemdb : Lean.Elab.Command.CommandElab

Equations

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