val mk_Exists (typ pred: term) : Tot formula
let mk_Exists (typ : term) (pred : term) : Tot formula =
    let b = pack_bv ({ ppname = as_ppname "x";
                       sort = seal typ;
                       index = 0; }) in
    Exists b typ (pack (Tv_App pred (pack (Tv_BVar b), Q_Explicit)))
val mk_Exists (typ pred: term) : Tot formula
let mk_Exists (typ pred: term) : Tot formula =
let b = pack_bv ({ ppname = as_ppname "x"; sort = seal typ; index = 0 }) in
Exists b typ (pack (Tv_App pred (pack (Tv_BVar b), Q_Explicit)))
FStar.Reflection.V2.Formula.fst.checked
prims.fst.checked FStar.Tactics.V2.Builtins.fsti.checked FStar.Tactics.NamedView.fsti.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.Common.fsti.checked FStar.Reflection.V2.Derived.fst.checked FStar.Reflection.V2.Data.fsti.checked FStar.Reflection.V2.Builtins.fsti.checked FStar.Reflection.Types.fsti.checked FStar.Reflection.Const.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Base.fst.checked
FStar.Reflection.V2.Formula.fst
FStar.Tactics.NamedView.term FStar.Reflection.V2.Formula.Exists FStar.Tactics.NamedView.pack FStar.Tactics.NamedView.Tv_App FStar.Pervasives.Native.Mktuple2 FStar.Reflection.Types.term FStar.Reflection.V2.Data.aqualv FStar.Tactics.NamedView.Tv_BVar FStar.Reflection.V2.Data.Q_Explicit FStar.Tactics.NamedView.bv FStar.Tactics.NamedView.pack_bv FStar.Reflection.V2.Data.Mkbv_view FStar.Sealed.seal FStar.Reflection.Types.typ FStar.Reflection.V2.Data.as_ppname FStar.Reflection.V2.Formula.formula
(*
   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.Reflection.V2.Formula

open FStar.List.Tot.Base

open FStar.Reflection.Types
open FStar.Reflection.Const
open FStar.Reflection.V2.Builtins
open FStar.Reflection.V2.Derived
open FStar.Reflection.V2.Data

open FStar.Tactics.Common
open FStar.Tactics.Effect
open FStar.Tactics.V2.Builtins
open FStar.Tactics.NamedView

///// Helpers (we cannot use the ones in Tactics.V2.Derived, those are for named views /////
private let rec inspect_unascribe (t:term) : Tac term_view =
  match inspect t with
  | Tv_AscribedT t _ _ _
  | Tv_AscribedC t _ _ _ ->
    inspect_unascribe t
  | tv -> tv

private let rec collect_app' (args : list argv) (t : term)
  : Tac (term * list argv) (decreases t) =
    match inspect_unascribe t with
    | Tv_App l r ->
        collect_app' (r::args) l
    | _ -> (t, args)

private let collect_app = collect_app' []
/////

[@@plugin]
noeq type comparison =
  | Eq     of option typ  (* Propositional equality (eq2), maybe annotated *)
  | BoolEq of option typ  (* Decidable, boolean equality (eq), maybe annotated *)
  | Lt | Le | Gt | Ge     (* Orderings, at type `int` (and subtypes) *)

[@@plugin]
noeq type formula =
  | True_  : formula
  | False_ : formula
  | Comp   : comparison -> term -> term -> formula
  | And    : term -> term -> formula
  | Or     : term -> term -> formula
  | Not    : term -> formula
  | Implies: term -> term -> formula
  | Iff    : term -> term -> formula
  | Forall : bv -> typ -> term -> formula
  | Exists : bv -> typ -> term -> formula
  | App    : term -> term -> formula
  | Name   : namedv -> formula
  | FV     : fv -> formula
  | IntLit : int -> formula
  | F_Unknown : formula // Also a baked-in "None"

let mk_Forall (typ : term) (pred : term) : Tot formula =
    let b = pack_bv ({ ppname = as_ppname "x";
                       sort = seal typ;
                       index = 0; }) in
    Forall b typ (pack (Tv_App pred (pack (Tv_BVar b), Q_Explicit)))
val mk_Exists (typ pred: term) : Tot formula
typ: FStar.Tactics.NamedView.term -> pred: FStar.Tactics.NamedView.term
  -> FStar.Reflection.V2.Formula.formula