source
opaque Lean.Elab.Tactic.Do.SpecAttr.mvcgenSimpExt :
Meta.SimpExtension

This attribute should not be used directly. It is an implementation detail of the `mvcgen` tactic.

source
def Lean.Elab.Tactic.Do.SpecAttr.getSpecSimpTheorems :
CoreM Meta.SimpTheorems

The simp set accumulated by the `@[spec]` attribute. (This does not include Hoare triple specs.) It is an implementation detail of the `mvcgen` tactic.

Equations

- Lean.Elab.Tactic.Do.SpecAttr.getSpecSimpTheorems = Lean.Elab.Tactic.Do.SpecAttr.mvcgenSimpExt.getTheorems

Instances For

source
inductive Lean.Elab.Tactic.Do.SpecAttr.SpecProof :
Type

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

Instances For

source
instance Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecProof :
Inhabited SpecProof
Equations

- Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecProof = { default := Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecProof.default }

source
def Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecProof.default :
SpecProof
Equations

- Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecProof.default = Lean.Elab.Tactic.Do.SpecAttr.SpecProof.global default

Instances For

source
def Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecProof.beq :
SpecProof → SpecProof → Bool
Equations

- One or more equations did not get rendered due to their size.
- Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecProof.beq (Lean.Elab.Tactic.Do.SpecAttr.SpecProof.global a) (Lean.Elab.Tactic.Do.SpecAttr.SpecProof.global b) = (a == b)
- Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecProof.beq (Lean.Elab.Tactic.Do.SpecAttr.SpecProof.local a) (Lean.Elab.Tactic.Do.SpecAttr.SpecProof.local b) = (a == b)
- Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecProof.beq x✝¹ x✝ = false

Instances For

source
instance Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecProof :
BEq SpecProof
Equations

- Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecProof = { beq := Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecProof.beq }

source
def Lean.Elab.Tactic.Do.SpecAttr.SpecProof.key :
SpecProof → Name

A unique identifier corresponding to the origin.

Equations

- (Lean.Elab.Tactic.Do.SpecAttr.SpecProof.global declName).key = declName
- (Lean.Elab.Tactic.Do.SpecAttr.SpecProof.local fvarId).key = fvarId.name
- (Lean.Elab.Tactic.Do.SpecAttr.SpecProof.stx id ref proof).key = id

Instances For

source
instance Lean.Elab.Tactic.Do.SpecAttr.instHashableSpecProof :
Hashable SpecProof
Equations

- Lean.Elab.Tactic.Do.SpecAttr.instHashableSpecProof = { hash := fun (sp : Lean.Elab.Tactic.Do.SpecAttr.SpecProof) => hash sp.key }

source
def Lean.Elab.Tactic.Do.SpecAttr.SpecProof.instantiate (proof : SpecProof) :
MetaM (Array Expr × Array BinderInfo × Expr × Expr)
Equations

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

Instances For

source
instance Lean.Elab.Tactic.Do.SpecAttr.instToMessageDataSpecProof :
ToMessageData SpecProof
Equations

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

source
structure Lean.Elab.Tactic.Do.SpecAttr.SpecTheorem :
Type

- keys : Array Meta.DiscrTree.Key
- prog : Expr

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

- proof : SpecProof

  The proof for the theorem.

- etaPotential : Nat

  If `etaPotential` is non-zero, then the precondition contains meta variables that can be instantiated after applying `mintro ∀s` `etaPotential` many times.

- priority : Nat

Instances For

source
def Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheorem.default :
SpecTheorem
Equations

- Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheorem.default = { keys := default, prog := default, proof := default, etaPotential := default, priority := default }

Instances For

source
instance Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheorem :
Inhabited SpecTheorem
Equations

- Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheorem = { default := Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheorem.default }

source
instance Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecTheorem :
BEq SpecTheorem
Equations

- Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecTheorem = { beq := Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecTheorem.beq }

source
def Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecTheorem.beq :
SpecTheorem → SpecTheorem → Bool
Equations

- One or more equations did not get rendered due to their size.
- Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecTheorem.beq x✝¹ x✝ = false

Instances For

source
@[reducible, inline]
abbrev Lean.Elab.Tactic.Do.SpecAttr.SpecEntry :
Type
Equations

- Lean.Elab.Tactic.Do.SpecAttr.SpecEntry = Lean.Elab.Tactic.Do.SpecAttr.SpecTheorem

Instances For

source
structure Lean.Elab.Tactic.Do.SpecAttr.SpecTheorems :
Type

- specs : Meta.DiscrTree SpecTheorem
- erased : PHashSet SpecProof

Instances For

source
instance Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheorems :
Inhabited SpecTheorems
Equations

- Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheorems = { default := Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheorems.default }

source
def Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheorems.default :
SpecTheorems
Equations

- Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheorems.default = { specs := default, erased := default }

Instances For

source
def Lean.Elab.Tactic.Do.SpecAttr.SpecTheorems.isErased (d : SpecTheorems) (thmId : SpecProof) :
Bool
Equations

- d.isErased thmId = Lean.PersistentHashSet.contains d.erased thmId

Instances For

source
def Lean.Elab.Tactic.Do.SpecAttr.SpecTheorems.eraseCore (d : SpecTheorems) (thmId : SpecProof) :
SpecTheorems
Equations

- d.eraseCore thmId = { specs := d.specs, erased := Lean.PersistentHashSet.insert d.erased thmId }

Instances For

source
@[reducible, inline]
abbrev Lean.Elab.Tactic.Do.SpecAttr.SpecExtension :
Type
Equations

- Lean.Elab.Tactic.Do.SpecAttr.SpecExtension = Lean.SimpleScopedEnvExtension Lean.Elab.Tactic.Do.SpecAttr.SpecEntry Lean.Elab.Tactic.Do.SpecAttr.SpecTheorems

Instances For

source
def Lean.Elab.Tactic.Do.SpecAttr.simpSPredConfig :
Meta.ConfigWithKey
Equations

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

Instances For

source
def Lean.Elab.Tactic.Do.SpecAttr.computeMVarBetaPotentialForSPred (xs : Array Expr) (σs e : Expr) :
MetaM Nat

If `σs : List Type`, then `e : SPred σs`. Return the number of times `e` needs to be applied in order to assign closed solutions to meta variables.

Equations

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

Instances For

source
def Lean.Elab.Tactic.Do.SpecAttr.mkSpecTheoremFromConst (declName : Name) (prio : Nat := 1000) :
MetaM SpecTheorem
Equations

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

Instances For

source
def Lean.Elab.Tactic.Do.SpecAttr.mkSpecTheoremFromLocal (fvar : FVarId) (prio : Nat := 1000) :
MetaM SpecTheorem
Equations

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

Instances For

source
def Lean.Elab.Tactic.Do.SpecAttr.mkSpecTheoremFromStx (ref : Syntax) (proof : Expr) (prio : Nat := 1000) :
MetaM SpecTheorem
Equations

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

Instances For

source
def Lean.Elab.Tactic.Do.SpecAttr.addSpecTheoremEntry (d : SpecTheorems) (e : SpecTheorem) :
SpecTheorems
Equations

- Lean.Elab.Tactic.Do.SpecAttr.addSpecTheoremEntry d e = { specs := d.specs.insertCore e.keys e, erased := d.erased }

Instances For

source
def Lean.Elab.Tactic.Do.SpecAttr.addSpecTheorem (ext : SpecExtension) (declName : Name) (prio : Nat) (attrKind : AttributeKind) :
MetaM Unit
Equations

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

Instances For

source
def Lean.Elab.Tactic.Do.SpecAttr.mkSpecExt :
SimpleScopedEnvExtension.Descr SpecEntry SpecTheorems
Equations

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

Instances For

source
opaque Lean.Elab.Tactic.Do.SpecAttr.specAttr :
SpecExtension
source
def Lean.Elab.Tactic.Do.SpecAttr.mkSpecAttr (ext : SpecExtension) :
AttributeImpl
Equations

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

Instances For

source
def Lean.Elab.Tactic.Do.SpecAttr.SpecExtension.getTheorems (ext : SpecExtension) :
CoreM SpecTheorems
Equations

- ext.getTheorems = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState ext __do_lift)

Instances For

source
def Lean.Elab.Tactic.Do.SpecAttr.getSpecTheorems :
CoreM SpecTheorems
Equations

- Lean.Elab.Tactic.Do.SpecAttr.getSpecTheorems = Lean.Elab.Tactic.Do.SpecAttr.specAttr.getTheorems

Instances For