Documentation

Lean.Meta.Tactic.Grind.Arith.Cutsat.Foreign

source
def Lean.Meta.Grind.Arith.Cutsat.mkForeignVar (e : Expr) (t : ForeignType) :
GoalM Var
Equations
    Instances For
      source
      def Lean.Meta.Grind.Arith.Cutsat.foreignTerm? (e : Expr) :
      GoalM (Option ForeignType)
      Equations
        Instances For
          source
          def Lean.Meta.Grind.Arith.Cutsat.hasForeignVar (e : Expr) :
          GoalM Bool
          Equations
            Instances For
              source
              def Lean.Meta.Grind.Arith.Cutsat.foreignTermOrLit? (e : Expr) :
              GoalM (Option ForeignType)
              Equations
                Instances For
                  source
                  def Lean.Meta.Grind.Arith.Cutsat.getForeignVars (t : ForeignType) :
                  GoalM (PArray Expr)
                  Equations
                    Instances For
                      source
                      def Lean.Meta.Grind.Arith.Cutsat.ForeignType.denoteType :
                      ForeignType → Expr
                      Equations
                        Instances For