def Loom.Tactic.SpecAttr.lspec : Lean.ParserDescr

opaque Loom.Tactic.SpecAttr.lspecSimpExt : Lean.Meta.SimpExtension

This attribute should not be used directly. It is an implementation detail of loom2 tactics.

def Loom.Tactic.SpecAttr.getSpecSimpTheorems : Lean.CoreM Lean.Meta.SimpTheorems

The simp set accumulated by the @[lspec] attribute. (This does not include Hoare triple specs.)

inductive Loom.Tactic.SpecAttr.SpecProof : Type

• global (declName : Lean.Name) : SpecProof
• local (fvarId : Lean.FVarId) : SpecProof
• stx (id : Lean.Name) (ref : Lean.Syntax) (proof : Lean.Expr) : SpecProof

@[implicit_reducible]

instance Loom.Tactic.SpecAttr.instInhabitedSpecProof : Inhabited SpecProof

def Loom.Tactic.SpecAttr.instInhabitedSpecProof.default : SpecProof

@[implicit_reducible]

instance Loom.Tactic.SpecAttr.instBEqSpecProof : BEq SpecProof

def Loom.Tactic.SpecAttr.instBEqSpecProof.beq : SpecProof → SpecProof → Bool

def Loom.Tactic.SpecAttr.SpecProof.key : SpecProof → Lean.Name

A unique identifier corresponding to the origin.

@[implicit_reducible]

instance Loom.Tactic.SpecAttr.instHashableSpecProof : Hashable SpecProof

def Loom.Tactic.SpecAttr.SpecProof.instantiate (proof : SpecProof) : Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr × Lean.Expr)

@[implicit_reducible]

instance Loom.Tactic.SpecAttr.instToMessageDataSpecProof : Lean.ToMessageData SpecProof

structure Loom.Tactic.SpecAttr.SpecTheorem : Type

• keys : Array Lean.Meta.DiscrTree.Key
• prog : Lean.Expr

  Expr key tested for matching, in ∀-quantified form. keys = (← mkPath (← forallMetaTelescope prog).2.2).

• pattern : Option Lean.Meta.Sym.Pattern

  Pattern for matching the program expression. Populated by migrateSpecTheoremsDatabase.

• proof : SpecProof

  The proof for the theorem.

• priority : Nat

@[implicit_reducible]

instance Loom.Tactic.SpecAttr.instInhabitedSpecTheorem : Inhabited SpecTheorem

def Loom.Tactic.SpecAttr.instInhabitedSpecTheorem.default : SpecTheorem

@[implicit_reducible]

instance Loom.Tactic.SpecAttr.instBEqSpecTheorem : BEq SpecTheorem

@[reducible, inline]

abbrev Loom.Tactic.SpecAttr.SpecEntry : Type

structure Loom.Tactic.SpecAttr.SpecTheorems : Type

• specs : Lean.Meta.DiscrTree SpecTheorem
• erased : Lean.PHashSet SpecProof

def Loom.Tactic.SpecAttr.instInhabitedSpecTheorems.default : SpecTheorems

@[implicit_reducible]

instance Loom.Tactic.SpecAttr.instInhabitedSpecTheorems : Inhabited SpecTheorems

def Loom.Tactic.SpecAttr.SpecTheorems.add (d : SpecTheorems) (e : SpecTheorem) : SpecTheorems

def Loom.Tactic.SpecAttr.SpecTheorems.isErased (d : SpecTheorems) (thmId : SpecProof) : Bool

def Loom.Tactic.SpecAttr.SpecTheorems.erase (d : SpecTheorems) (thmId : SpecProof) : SpecTheorems

@[reducible, inline]

abbrev Loom.Tactic.SpecAttr.SpecExtension : Type

def Loom.Tactic.SpecAttr.mkSpecTheoremFromConst (declName : Lean.Name) (prio : Nat := 1000) : Lean.MetaM SpecTheorem

def Loom.Tactic.SpecAttr.mkSpecTheoremFromLocal (fvar : Lean.FVarId) (prio : Nat := 1000) : Lean.MetaM SpecTheorem

def Loom.Tactic.SpecAttr.mkSpecTheoremFromStx (ref : Lean.Syntax) (proof : Lean.Expr) (prio : Nat := 1000) : Lean.MetaM SpecTheorem

def Loom.Tactic.SpecAttr.SpecExtension.addSpecTheoremFromConst (ext : SpecExtension) (declName : Lean.Name) (prio : Nat) (attrKind : Lean.AttributeKind) : Lean.MetaM Unit

def Loom.Tactic.SpecAttr.SpecExtension.addSpecTheoremFromLocal (ext : SpecExtension) (fvar : Lean.FVarId) (prio : Nat := 1000) : Lean.MetaM Unit

def Loom.Tactic.SpecAttr.mkSpecExt : Lean.SimpleScopedEnvExtension.Descr SpecEntry SpecTheorems

opaque Loom.Tactic.SpecAttr.lspecAttr : SpecExtension

def Loom.Tactic.SpecAttr.mkLSpecAttr (ext : SpecExtension) : Lean.AttributeImpl

def Loom.Tactic.SpecAttr.SpecExtension.getTheorems (ext : SpecExtension) : Lean.CoreM SpecTheorems

def Loom.Tactic.SpecAttr.getSpecTheorems : Lean.CoreM SpecTheorems