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

def Auto.instBEqLemDB.beq : LemDB → LemDB → Bool

Equations

• Auto.instBEqLemDB.beq Auto.LemDB.empty Auto.LemDB.empty = true
• Auto.instBEqLemDB.beq (Auto.LemDB.addLemma a a_1) (Auto.LemDB.addLemma b b_1) = (a == b && Auto.instBEqLemDB.beq a_1 b_1)
• Auto.instBEqLemDB.beq (Auto.LemDB.compose a) (Auto.LemDB.compose b) = (a == b)
• Auto.instBEqLemDB.beq x✝¹ x✝ = false

instance Auto.instBEqLemDB : BEq LemDB

Equations

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

instance Auto.instHashableLemDB : Hashable LemDB

Equations

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

def Auto.instHashableLemDB.hash : LemDB → UInt64

Equations

• Auto.instHashableLemDB.hash Auto.LemDB.empty = 0
• Auto.instHashableLemDB.hash (Auto.LemDB.addLemma a a_1) = mixHash (mixHash 1 (hash a)) (Auto.instHashableLemDB.hash a_1)
• Auto.instHashableLemDB.hash (Auto.LemDB.compose a) = mixHash 2 (hash a)

def Auto.instInhabitedLemDB.default : LemDB

Equations

• Auto.instInhabitedLemDB.default = Auto.LemDB.empty

instance Auto.instInhabitedLemDB : Inhabited LemDB

Equations

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

def Auto.instReprLemDB.repr : LemDB → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Auto.instReprLemDB.repr Auto.LemDB.empty prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Auto.LemDB.empty")).group prec✝

instance Auto.instReprLemDB : Repr LemDB

Equations

• Auto.instReprLemDB = { reprPrec := Auto.instReprLemDB.repr }

@[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.