val notAscription (tv: named_term_view) : bool
let notAscription (tv:named_term_view) : bool =
  not (Tv_AscribedT? tv) && not (Tv_AscribedC? tv)
val notAscription (tv: named_term_view) : bool
let notAscription (tv: named_term_view) : bool =
not (Tv_AscribedT? tv) && not (Tv_AscribedC? tv)
FStar.Tactics.NamedView.fsti.checked
prims.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Reflection.V2.Data.fsti.checked FStar.Reflection.V2.fst.checked FStar.Range.fsti.checked FStar.Pervasives.fsti.checked
FStar.Tactics.NamedView.fsti
FStar.Tactics.NamedView.named_term_view Prims.op_AmpAmp Prims.op_Negation FStar.Tactics.NamedView.uu___is_Tv_AscribedT FStar.Tactics.NamedView.uu___is_Tv_AscribedC Prims.bool
(*
   Copyright 2008-2023 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.NamedView

open FStar.Tactics.Effect
open FStar.Reflection.V2
open FStar.Reflection.V2.Data
module R = FStar.Reflection.V2

(* Re export the syntax types. Expose variables as their views, users do
not need to pack/inspect these if they are using the named view. *)
type namedv   = R.namedv_view
type bv       = R.bv_view
type comp     = R.comp_view
type binding  = R.binding (* already good *)
(* Terms and universes are still *deep*, so we do not change their
representation, and the user needs to pack/inspect. *)
type term     = R.term
type universe = R.universe

[@@plugin]
noeq
type binder = {
  uniq   : nat;

  ppname : ppname_t;
  sort   : R.typ;
  qual   : aqualv;
  attrs  : list term;
}
type binders = list binder

let is_simple_binder (b:binder) = Q_Explicit? b.qual /\ Nil? b.attrs
type simple_binder = b:binder{is_simple_binder b}

type univ_name = string & Range.range

[@@plugin]
noeq
type named_universe_view =
  | Uv_Zero : named_universe_view
  | Uv_Succ : universe -> named_universe_view
  | Uv_Max  : universes -> named_universe_view
  | Uv_BVar : nat -> named_universe_view
  | Uv_Name : univ_name -> named_universe_view
  | Uv_Unif : R.universe_uvar -> named_universe_view
  | Uv_Unk  : named_universe_view

[@@plugin]
noeq
type pattern =
 // A built-in constant
 | Pat_Constant {
     c : vconst
   }

 // A fully applied constructor, each boolean marks whether the
 // argument was an explicitly-provided implicit argument
 | Pat_Cons {
     head    : fv;
     univs   : option universes;
     subpats : list (pattern * bool)
   }

 // A pattern-bound *named* variable.
 | Pat_Var {
     v    : namedv;
     sort : sealed typ;
   }

 // Dot pattern: resolved by other elements in the pattern and type
 | Pat_Dot_Term {
     t : option term;
   }

type branch = pattern & term
type match_returns_ascription = binder & (either term comp & option term & bool)

[@@plugin]
noeq
type named_term_view =
  | Tv_Var    : v:namedv -> named_term_view
  | Tv_BVar   : v:bv -> named_term_view
  | Tv_FVar   : v:fv -> named_term_view
  | Tv_UInst  : v:fv -> us:universes -> named_term_view
  | Tv_App    : hd:term -> a:argv -> named_term_view
  | Tv_Abs    : bv:binder -> body:term -> named_term_view
  | Tv_Arrow  : bv:binder -> c:comp -> named_term_view
  | Tv_Type   : universe -> named_term_view
  | Tv_Refine : b:simple_binder -> ref:term -> named_term_view
  | Tv_Const  : vconst -> named_term_view
  | Tv_Uvar   : nat -> ctx_uvar_and_subst -> named_term_view
  | Tv_Let    : recf:bool -> attrs:(list term) -> b:simple_binder -> def:term -> body:term -> named_term_view
  | Tv_Match  : scrutinee:term -> ret:option match_returns_ascription -> brs:(list branch) -> named_term_view
  | Tv_AscribedT : e:term -> t:term -> tac:option term -> use_eq:bool -> named_term_view
  | Tv_AscribedC : e:term -> c:comp -> tac:option term -> use_eq:bool -> named_term_view
  | Tv_Unknown  : named_term_view // An underscore: _
  | Tv_Unsupp : named_term_view // failed to inspect, not supported

// Repeat from FStar.R.Data
val notAscription (tv: named_term_view) : bool
tv: FStar.Tactics.NamedView.named_term_view -> Prims.bool