val notAscription (tv: term_view) : bool
let notAscription (tv:term_view) : bool =
  not (Tv_AscribedT? tv) && not (Tv_AscribedC? tv)
val notAscription (tv: term_view) : bool
let notAscription (tv: term_view) : bool =
not (Tv_AscribedT? tv) && not (Tv_AscribedC? tv)
FStar.Reflection.V1.Data.fsti.checked
prims.fst.checked FStar.Sealed.Inhabited.fst.checked FStar.Reflection.V2.Data.fsti.checked FStar.Reflection.V2.Builtins.fsti.checked FStar.Reflection.Types.fsti.checked FStar.Pervasives.fsti.checked
FStar.Reflection.V1.Data.fsti
FStar.Reflection.V1.Data.term_view Prims.op_AmpAmp Prims.op_Negation FStar.Reflection.V1.Data.uu___is_Tv_AscribedT FStar.Reflection.V1.Data.uu___is_Tv_AscribedC Prims.bool
(*
   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.V1.Data

(* What's this!? Well, the compiler now works fully with V2, so whenever
we need to reason/extract a term, we need things like V2.Tv_App and V2.pack_ln
in scope. So, force them into scope here. *)
module X = FStar.Reflection.V2.Data
module X = FStar.Reflection.V2.Builtins

open FStar.Reflection.Types

(* V1 does not really use the primitive ident type, but this
explicit pair of string & range *)
type ident = string & range
type univ_name = ident

noeq
type vconst =
  | C_Unit      : vconst
  | C_Int       : int -> vconst // Not exposing the full details of our integer repr.
  | C_True      : vconst
  | C_False     : vconst
  | C_String    : string -> vconst
  | C_Range     : range -> vconst
  | C_Reify     : vconst
  | C_Reflect   : name -> vconst
  (* TODO: complete *)

type universes = list universe

// This is shadowing `pattern` from Prims (for smt_pats)
noeq
type pattern =
    | Pat_Constant : vconst -> pattern              // A built-in constant
    | Pat_Cons     : fv -> option universes -> list (pattern * bool) -> pattern
                                                    // A fully applied constructor, each boolean marks
                                                    // whether the argument was an explicitly-provided
                                                    // implicit argument
    | Pat_Var      : bv -> sealed typ -> pattern    // Pattern bound variable
    | Pat_Dot_Term : option term -> pattern         // Dot pattern: resolved by other elements in the pattern and type

type branch = pattern * term  // | pattern -> term

noeq
type aqualv =
    | Q_Implicit
    | Q_Explicit
    | Q_Meta of term

type argv = term * aqualv

(* The type of a string observable only with a tactic.
   All values of type ppname_t are provably equal *)
let ppname_t = FStar.Sealed.Inhabited.sealed ""
let as_ppname (x:string) : ppname_t = FStar.Sealed.Inhabited.seal x

noeq
type bv_view = {
    bv_ppname : ppname_t;
    bv_index : nat;
}

noeq
type binder_view = {
  binder_bv : bv;
  binder_qual : aqualv;
  binder_attrs : list term;
  binder_sort : typ;
}

noeq
type universe_view =
  | Uv_Zero : universe_view
  | Uv_Succ : universe -> universe_view
  | Uv_Max  : universes -> universe_view
  | Uv_BVar : nat -> universe_view
  | Uv_Name : univ_name -> universe_view
  | Uv_Unif : universe_uvar -> universe_view
  | Uv_Unk  : universe_view

noeq
type term_view =
  | Tv_Var    : v:bv -> term_view
  | Tv_BVar   : v:bv -> term_view
  | Tv_FVar   : v:fv -> term_view
  | Tv_UInst  : v:fv -> us:universes -> term_view
  | Tv_App    : hd:term -> a:argv -> term_view
  | Tv_Abs    : bv:binder -> body:term -> term_view
  | Tv_Arrow  : bv:binder -> c:comp -> term_view
  | Tv_Type   : universe -> term_view
  | Tv_Refine : bv:bv -> sort:typ -> ref:term -> term_view
  | Tv_Const  : vconst -> term_view
  | Tv_Uvar   : nat -> ctx_uvar_and_subst -> term_view
  | Tv_Let    : recf:bool -> attrs:(list term) -> bv:bv -> ty:typ -> def:term -> body:term -> term_view
  | Tv_Match  : scrutinee:term -> ret:option match_returns_ascription -> brs:(list branch) -> term_view
  | Tv_AscribedT : e:term -> t:term -> tac:option term -> use_eq:bool -> term_view
  | Tv_AscribedC : e:term -> c:comp -> tac:option term -> use_eq:bool -> term_view
  | Tv_Unknown  : term_view // An underscore: _
  | Tv_Unsupp : term_view // failed to inspect, not supported
val notAscription (tv: term_view) : bool
tv: FStar.Reflection.V1.Data.term_view -> Prims.bool