val binding_to_namedv (b: binding) : Tot namedv
let binding_to_namedv (b : binding) : Tot namedv =
  {
    ppname = b.ppname;
    sort   = seal b.sort;
    uniq   = b.uniq
  }
val binding_to_namedv (b: binding) : Tot namedv
let binding_to_namedv (b: binding) : Tot namedv =
{ ppname = b.ppname; sort = seal b.sort; uniq = b.uniq }
FStar.Tactics.V2.SyntaxCoercions.fst.checked
prims.fst.checked FStar.Tactics.NamedView.fsti.checked FStar.Tactics.Builtins.fst.checked FStar.Sealed.fsti.checked FStar.Pervasives.fsti.checked
FStar.Tactics.V2.SyntaxCoercions.fst
FStar.Tactics.NamedView.binding FStar.Reflection.V2.Data.Mknamedv_view FStar.Reflection.V2.Data.__proj__Mkbinding__item__uniq FStar.Sealed.seal FStar.Reflection.Types.typ FStar.Reflection.V2.Data.__proj__Mkbinding__item__sort FStar.Reflection.V2.Data.__proj__Mkbinding__item__ppname FStar.Tactics.NamedView.namedv
module FStar.Tactics.V2.SyntaxCoercions

open FStar.Tactics.Builtins
open FStar.Tactics.NamedView
open FStar.Sealed

[@@coercion]
let namedv_to_term (x : namedv) : Tot term =
  pack (Tv_Var x)

[@@coercion]
let binder_to_namedv (b : binder) : Tot namedv =
  {
    ppname = b.ppname;
    uniq   = b.uniq;
    sort   = seal b.sort;
  }

[@@coercion]
let binder_to_term (b : binder) : Tot term =
  pack (Tv_Var (binder_to_namedv b))

[@@coercion]
let binding_to_namedv (b : binding) : Tot namedv =
val binding_to_namedv (b: binding) : Tot namedv
b: FStar.Tactics.NamedView.binding -> FStar.Tactics.NamedView.namedv