Documentation

VCVio.ProgramLogic.Tactics.Common.CompiledRules

Compiled Program-Logic Rules #

This module packages registered unary and relational VC-spec rules into compact compiled forms used by the vcstep and rvcstep tactic infrastructure.

source
inductive OracleComp.ProgramLogic.UnaryRuleApplicationMode :
Type
Instances For
    source
    def OracleComp.ProgramLogic.instInhabitedUnaryRuleApplicationMode.default :
    UnaryRuleApplicationMode
    Instances For
      source
      @[implicit_reducible]
      instance OracleComp.ProgramLogic.instInhabitedUnaryRuleApplicationMode :
      Inhabited UnaryRuleApplicationMode
      source
      def OracleComp.ProgramLogic.instBEqUnaryRuleApplicationMode.beq :
      UnaryRuleApplicationMode → UnaryRuleApplicationMode → Bool
      Instances For
        source
        @[implicit_reducible]
        instance OracleComp.ProgramLogic.instBEqUnaryRuleApplicationMode :
        BEq UnaryRuleApplicationMode
        source
        def OracleComp.ProgramLogic.instReprUnaryRuleApplicationMode.repr :
        UnaryRuleApplicationMode → ℕ → Std.Format
        Instances For
          source
          @[implicit_reducible]
          instance OracleComp.ProgramLogic.instReprUnaryRuleApplicationMode :
          Repr UnaryRuleApplicationMode
          source
          inductive OracleComp.ProgramLogic.RelationalRuleApplicationMode :
          Type
          Instances For
            source
            @[implicit_reducible]
            instance OracleComp.ProgramLogic.instInhabitedRelationalRuleApplicationMode :
            Inhabited RelationalRuleApplicationMode
            source
            def OracleComp.ProgramLogic.instInhabitedRelationalRuleApplicationMode.default :
            RelationalRuleApplicationMode
            Instances For
              source
              @[implicit_reducible]
              instance OracleComp.ProgramLogic.instBEqRelationalRuleApplicationMode :
              BEq RelationalRuleApplicationMode
              source
              def OracleComp.ProgramLogic.instBEqRelationalRuleApplicationMode.beq :
              RelationalRuleApplicationMode → RelationalRuleApplicationMode → Bool
              Instances For
                source
                @[implicit_reducible]
                instance OracleComp.ProgramLogic.instReprRelationalRuleApplicationMode :
                Repr RelationalRuleApplicationMode
                source
                def OracleComp.ProgramLogic.instReprRelationalRuleApplicationMode.repr :
                RelationalRuleApplicationMode → ℕ → Std.Format
                Instances For
                  source
                  structure OracleComp.ProgramLogic.CompiledUnaryVCSpecRule :
                  Type
                  Instances For
                    source
                    @[implicit_reducible]
                    instance OracleComp.ProgramLogic.instInhabitedCompiledUnaryVCSpecRule :
                    Inhabited CompiledUnaryVCSpecRule
                    source
                    def OracleComp.ProgramLogic.instInhabitedCompiledUnaryVCSpecRule.default :
                    CompiledUnaryVCSpecRule
                    Instances For
                      source
                      @[implicit_reducible]
                      instance OracleComp.ProgramLogic.instReprCompiledUnaryVCSpecRule :
                      Repr CompiledUnaryVCSpecRule
                      source
                      def OracleComp.ProgramLogic.instReprCompiledUnaryVCSpecRule.repr :
                      CompiledUnaryVCSpecRule → ℕ → Std.Format
                      Instances For
                        source
                        structure OracleComp.ProgramLogic.CompiledRelationalVCSpecRule :
                        Type
                        Instances For
                          source
                          def OracleComp.ProgramLogic.instInhabitedCompiledRelationalVCSpecRule.default :
                          CompiledRelationalVCSpecRule
                          Instances For
                            source
                            @[implicit_reducible]
                            instance OracleComp.ProgramLogic.instInhabitedCompiledRelationalVCSpecRule :
                            Inhabited CompiledRelationalVCSpecRule
                            source
                            @[implicit_reducible]
                            instance OracleComp.ProgramLogic.instReprCompiledRelationalVCSpecRule :
                            Repr CompiledRelationalVCSpecRule
                            source
                            def OracleComp.ProgramLogic.instReprCompiledRelationalVCSpecRule.repr :
                            CompiledRelationalVCSpecRule → ℕ → Std.Format
                            Instances For
                              source
                              def OracleComp.ProgramLogic.CompiledUnaryVCSpecRule.theoremName (rule : CompiledUnaryVCSpecRule) :
                              Lean.Name
                              Instances For
                                source
                                def OracleComp.ProgramLogic.CompiledUnaryVCSpecRule.kind (rule : CompiledUnaryVCSpecRule) :
                                VCSpecKind
                                Instances For
                                  source
                                  def OracleComp.ProgramLogic.CompiledUnaryVCSpecRule.replayText (rule : CompiledUnaryVCSpecRule) :
                                  String
                                  Instances For
                                    source
                                    def OracleComp.ProgramLogic.CompiledUnaryVCSpecRule.canUseConsequence (rule : CompiledUnaryVCSpecRule) :
                                    Bool
                                    Instances For
                                      source
                                      def OracleComp.ProgramLogic.CompiledRelationalVCSpecRule.theoremName (rule : CompiledRelationalVCSpecRule) :
                                      Lean.Name
                                      Instances For
                                        source
                                        def OracleComp.ProgramLogic.CompiledRelationalVCSpecRule.kind (rule : CompiledRelationalVCSpecRule) :
                                        VCSpecKind
                                        Instances For
                                          source
                                          def OracleComp.ProgramLogic.CompiledRelationalVCSpecRule.replayText (rule : CompiledRelationalVCSpecRule) :
                                          String
                                          Instances For
                                            source
                                            def OracleComp.ProgramLogic.CompiledRelationalVCSpecRule.canUseConsequence (rule : CompiledRelationalVCSpecRule) :
                                            Bool
                                            Instances For
                                              source
                                              def OracleComp.ProgramLogic.compileUnaryVCSpecRule? (entry : VCSpecEntry) :
                                              Option CompiledUnaryVCSpecRule
                                              Instances For
                                                source
                                                def OracleComp.ProgramLogic.compileUnaryVCSpecRules (entries : Array VCSpecEntry) :
                                                Array CompiledUnaryVCSpecRule
                                                Instances For
                                                  source
                                                  def OracleComp.ProgramLogic.compileRelationalVCSpecRule? (entry : VCSpecEntry) :
                                                  Option CompiledRelationalVCSpecRule
                                                  Instances For
                                                    source
                                                    def OracleComp.ProgramLogic.compileRelationalVCSpecRules (entries : Array VCSpecEntry) :
                                                    Array CompiledRelationalVCSpecRule
                                                    Instances For
                                                      source
                                                      def OracleComp.ProgramLogic.getCompiledUnaryVCSpecRules (comp : Lean.Expr) :
                                                      Lean.MetaM (Array CompiledUnaryVCSpecRule)
                                                      Instances For
                                                        source
                                                        def OracleComp.ProgramLogic.getCompiledUnaryVCSpecRulesOfKind (kind : VCSpecKind) :
                                                        Lean.CoreM (Array CompiledUnaryVCSpecRule)
                                                        Instances For
                                                          source
                                                          def OracleComp.ProgramLogic.getCompiledRelationalVCSpecRules (oa ob : Lean.Expr) :
                                                          Lean.MetaM (Array CompiledRelationalVCSpecRule)
                                                          Instances For
                                                            source
                                                            def OracleComp.ProgramLogic.getCompiledRelationalVCSpecRulesOfKind (kind : VCSpecKind) :
                                                            Lean.CoreM (Array CompiledRelationalVCSpecRule)
                                                            Instances For