Documentation

Blaster.Smt.Translate

source
def Blaster.Smt.translateExpr (e : Lean.Expr) (topLevel : Bool := true) :
Optimize.TranslateEnvT SmtTerm

Translate an optimized Lean4 Expr to an SMT term, and invoke the solver. -

Equations
Instances For
    source
    partial def Blaster.Smt.translateExpr.visit (e : Lean.Expr) (topLevel : Bool := false) :
    Optimize.TranslateEnvT SmtTerm
    source
    def Blaster.Smt.Translate.main (e : Lean.Expr) (logUndetermined : Bool := true) :
    Optimize.TranslateEnvT (Result × Lean.Expr)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Blaster.Smt.Translate.main.isTheoremExpr (e : Lean.Expr) :
      Optimize.TranslateEnvT (Option Lean.Expr)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Blaster.Smt.Translate.main.toPropExpr (e : Lean.Expr) :
        Optimize.TranslateEnvT Lean.Expr
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Blaster.Smt.Translate.main.addAxioms (e : Lean.Expr) (axioms : List Lean.Expr) :
          Optimize.TranslateEnvT Lean.Expr
          Equations
          Instances For
            source
            def Blaster.Smt.command (sOpts : Options.BlasterOptions) (stx : Lean.Syntax) :
            Lean.Elab.TermElabM Unit
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For