Documentation

Lean.Elab.Tactic.Do.Internal.VCGen.FrameProcAttr

The @[frameproc] attribute registers FrameProcs for vcgen.

source
unsafe def Lean.Elab.Tactic.Do.Internal.VCGen.getFrameProcFromDeclImpl (declName : Name) :
ImportM FrameProc
Instances For
    source
    @[implemented_by Lean.Elab.Tactic.Do.Internal.VCGen.getFrameProcFromDeclImpl]
    opaque Lean.Elab.Tactic.Do.Internal.VCGen.getFrameProcFromDecl (declName : Name) :
    ImportM FrameProc

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

    source
    @[reducible, inline]
    abbrev Lean.Elab.Tactic.Do.Internal.VCGen.FrameProcExtension :
    Type
    Instances For
      source
      def Lean.Elab.Tactic.Do.Internal.VCGen.toFrameProcEntry (declName : Name) :
      ImportM (Name × FrameProc)
      Instances For
        source
        opaque Lean.Elab.Tactic.Do.Internal.VCGen.frameProcExt :
        FrameProcExtension
        source
        def Lean.Elab.Tactic.Do.Internal.VCGen.getFrameProcs {m : Type → Type} [Monad m] [MonadEnv m] :
        m FrameProcs

        The frame inference procedures in scope.

        Instances For
          source
          def Lean.Elab.Tactic.Do.Internal.VCGen.addFrameProcAttr (declName : Name) (kind : AttributeKind) :
          AttrM Unit
          Instances For