Documentation

GeneralizationLinter.Core.Verify

Verification #

source
def GeneralizationLinter.suppressingDiagnostics {m : Type → Type} {α : Type} [Monad m] [MonadFinally m] [Lean.MonadWithOptions m] [MonadLiftT Lean.CoreM m] (act : m α) :
m α

Run act quietly. When we run a verification gate, candidates that are rejected would emit warnings that we don't want to bother the user with.

Implementation notes

We turn off Elab.async because asynchronicity would make it impossible for us to ensure we capture the emitted messages.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def GeneralizationLinter.weakeningHolds (declInfo : Lean.ConstantInfo) (c : Candidate) :
    Lean.MetaM Bool
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      structure GeneralizationLinter.ConfirmedWeakening :
      Type
      • candidate : Candidate

        A verified weakening candidate.

      Instances For
        source
        def GeneralizationLinter.meetCandidates (config : LinterConfig) (G : ClassGraph) (declInfo : Lean.ConstantInfo) :
        Lean.MetaM (Array Candidate)

        Returns unverified weakening suggestion candidates for a given declaration.

        Implementation notes

        #TODO

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def GeneralizationLinter.getConfirmedWeakenings (config : LinterConfig) (G : ClassGraph) (declName : Lean.Name) :
          Lean.MetaM (Array ConfirmedWeakening)

          Returns verified weakening suggestions for a given declaration.

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