val split_arith : unit -> Tac unit
let rec split_arith () =
    if is_arith_goal () then
        begin
        prune "";
        addns "Prims";
        smt ()
        end
    else begin
        let g = cur_goal () in
        match term_as_formula g with
        | True_ ->
            trivial ()
        | And l r ->
            seq FStar.Tactics.split split_arith
        | Implies p q ->
            let _ = implies_intro () in
            seq split_arith l_revert
        | Forall _x _sort _p ->
            let bs = forall_intros () in
            seq split_arith (fun () -> l_revert_all bs)
        | _ ->
            ()
    end
val split_arith : unit -> Tac unit
let rec split_arith () =
if is_arith_goal ()
then
  (prune "";
    addns "Prims";
    smt ())
else
  let g = cur_goal () in
  match term_as_formula g with
  | True_ -> trivial ()
  | And l r -> seq FStar.Tactics.split split_arith
  | Implies p q ->
    let _ = implies_intro () in
    seq split_arith l_revert
  | Forall _x _sort _p ->
    let bs = forall_intros () in
    seq split_arith (fun () -> l_revert_all bs)
  | _ -> ()
FStar.Tactics.Arith.fst.checked
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.fst.checked FStar.Reflection.V2.Formula.fst.checked FStar.Reflection.V2.Arith.fst.checked FStar.Pervasives.fsti.checked
FStar.Tactics.Arith.fst
Prims.unit FStar.Tactics.V2.Derived.smt FStar.Tactics.V2.Builtins.addns FStar.Tactics.V2.Builtins.prune Prims.bool FStar.Tactics.V2.Derived.trivial FStar.Tactics.NamedView.term FStar.Tactics.V2.Derived.seq FStar.Tactics.V1.Logic.split FStar.Tactics.Arith.split_arith FStar.Tactics.V2.Logic.l_revert FStar.Tactics.NamedView.binding FStar.Tactics.V2.Logic.implies_intro FStar.Tactics.NamedView.bv FStar.Reflection.Types.typ FStar.Tactics.V2.Logic.l_revert_all Prims.list FStar.Tactics.V2.Logic.forall_intros FStar.Reflection.V2.Formula.formula FStar.Reflection.V2.Formula.term_as_formula FStar.Tactics.V2.Derived.cur_goal FStar.Tactics.Arith.is_arith_goal
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module FStar.Tactics.Arith

open FStar.Tactics.V2
open FStar.Reflection.V2.Formula
open FStar.Reflection.V2.Arith

// decide if the current goal is arith, drop the built representation of it
let is_arith_goal () : Tac bool =
    let g = cur_goal () in
    match run_tm (is_arith_prop g) with
    | Inr _ -> true
    | _ -> false

val split_arith : unit -> Tac unit
val split_arith : unit -> Tac unit
_: Prims.unit -> FStar.Tactics.Effect.Tac Prims.unit