let is_simple_binder (b:binder) = Q_Explicit? b.qual /\ Nil? b.attrs
let is_simple_binder (b: binder) =
Q_Explicit? b.qual /\ Nil? b.attrs
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.binder Prims.l_and Prims.b2t FStar.Reflection.V2.Data.uu___is_Q_Explicit FStar.Tactics.NamedView.__proj__Mkbinder__item__qual Prims.uu___is_Nil FStar.Tactics.NamedView.term FStar.Tactics.NamedView.__proj__Mkbinder__item__attrs Prims.logical
(*
   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
val is_simple_binder : b: FStar.Tactics.NamedView.binder -> Prims.logical
b: FStar.Tactics.NamedView.binder -> Prims.logical