The @[frameproc] attribute registers FrameProcs for vcgen.

unsafe def Lean.Elab.Tactic.VCGen.getFrameProcFromDeclImpl (declName : Name) : ImportM FrameProc

Equations

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

@[implemented_by Lean.Elab.Tactic.VCGen.getFrameProcFromDeclImpl]

opaque Lean.Elab.Tactic.VCGen.getFrameProcFromDecl (declName : Name) : ImportM FrameProc

Recover the compiled FrameProc value of a @[frameproc]-annotated declaration.

@[reducible, inline]

abbrev Lean.Elab.Tactic.VCGen.FrameProcExtension : Type

Equations

• Lean.Elab.Tactic.VCGen.FrameProcExtension = Lean.ScopedEnvExtension Lean.Name (Lean.Name × Lean.Elab.Tactic.VCGen.FrameProc) Lean.Elab.Tactic.VCGen.FrameProcs

def Lean.Elab.Tactic.VCGen.toFrameProcEntry (declName : Name) : ImportM (Name × FrameProc)

Equations

• Lean.Elab.Tactic.VCGen.toFrameProcEntry declName = do let __do_lift ← Lean.Elab.Tactic.VCGen.getFrameProcFromDecl declName pure (declName, __do_lift)

opaque Lean.Elab.Tactic.VCGen.frameProcExt : FrameProcExtension

def Lean.Elab.Tactic.VCGen.getFrameProcs {m : Type → Type} [Monad m] [MonadEnv m] : m FrameProcs

The frame inference procedures in scope.

Equations

• Lean.Elab.Tactic.VCGen.getFrameProcs = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Elab.Tactic.VCGen.frameProcExt __do_lift)

def Lean.Elab.Tactic.VCGen.addFrameProcAttr (declName : Name) (kind : AttributeKind) : AttrM Unit

Equations

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