Documentation

VCVio.ProgramLogic.Tactics.Common.Registry

VCSpec Registry #

Shared registry structures for looking up VC specification lemmas by head symbol.

source
structure OracleComp.ProgramLogic.VCSpecEntry :
Type
Instances For
    source
    def OracleComp.ProgramLogic.instInhabitedVCSpecEntry.default :
    VCSpecEntry
    Instances For
      source
      @[implicit_reducible]
      instance OracleComp.ProgramLogic.instInhabitedVCSpecEntry :
      Inhabited VCSpecEntry
      source
      def OracleComp.ProgramLogic.instBEqVCSpecEntry.beq :
      VCSpecEntry → VCSpecEntry → Bool
      Instances For
        source
        @[implicit_reducible]
        instance OracleComp.ProgramLogic.instBEqVCSpecEntry :
        BEq VCSpecEntry
        source
        @[implicit_reducible]
        instance OracleComp.ProgramLogic.instReprVCSpecEntry :
        Repr VCSpecEntry
        source
        def OracleComp.ProgramLogic.instReprVCSpecEntry.repr :
        VCSpecEntry → ℕ → Std.Format
        Instances For
          source
          def OracleComp.ProgramLogic.VCSpecEntry.kind (entry : VCSpecEntry) :
          VCSpecKind
          Instances For
            source
            def OracleComp.ProgramLogic.VCSpecEntry.lookupKey (entry : VCSpecEntry) :
            VCSpecLookupKey
            Instances For
              source
              structure OracleComp.ProgramLogic.VCSpecRegistry :
              Type
              Instances For
                source
                def OracleComp.ProgramLogic.instInhabitedVCSpecRegistry.default :
                VCSpecRegistry
                Instances For
                  source
                  @[implicit_reducible]
                  instance OracleComp.ProgramLogic.instInhabitedVCSpecRegistry :
                  Inhabited VCSpecRegistry
                  source
                  opaque OracleComp.ProgramLogic.vcSpecRegistry :
                  Lean.SimpleScopedEnvExtension VCSpecEntry VCSpecRegistry
                  source
                  def OracleComp.ProgramLogic.getRegisteredUnaryVCSpecEntries (comp : Lean.Expr) :
                  Lean.MetaM (Array VCSpecEntry)
                  Instances For
                    source
                    def OracleComp.ProgramLogic.getRegisteredRelationalVCSpecEntries (oa ob : Lean.Expr) :
                    Lean.MetaM (Array VCSpecEntry)
                    Instances For
                      source
                      def OracleComp.ProgramLogic.getRegisteredUnaryVCSpecTheorems (comp : Lean.Expr) :
                      Lean.MetaM (Array Lean.Name)
                      Instances For
                        source
                        def OracleComp.ProgramLogic.getRegisteredRelationalVCSpecTheorems (oa ob : Lean.Expr) :
                        Lean.MetaM (Array Lean.Name)
                        Instances For
                          source
                          def OracleComp.ProgramLogic.getVCSpecEntriesOfKind (kind : VCSpecKind) :
                          Lean.CoreM (Array VCSpecEntry)
                          Instances For
                            source
                            def OracleComp.ProgramLogic.getVCSpecTheoremsOfKind (kind : VCSpecKind) :
                            Lean.CoreM (Array Lean.Name)
                            Instances For
                              source
                              def OracleComp.ProgramLogic.getNormalizedUnaryVCSpecs (comp : Lean.Expr) :
                              Lean.MetaM (Array NormalizedVCSpec)
                              Instances For
                                source
                                def OracleComp.ProgramLogic.getNormalizedRelationalVCSpecs (oa ob : Lean.Expr) :
                                Lean.MetaM (Array NormalizedVCSpec)
                                Instances For