val assoc (#a: eqtype) (#b: _) (x: a) (l: list (a & b)) : Tac b
let assoc (#a: eqtype) #b (x: a) (l: list (a & b)): Tac b =
  match List.Tot.assoc x l with
  | Some x -> x
  | None -> fail "failure: assoc"
val assoc (#a: eqtype) (#b: _) (x: a) (l: list (a & b)) : Tac b
let assoc (#a: eqtype) #b (x: a) (l: list (a & b)) : Tac b =
match List.Tot.assoc x l with
| Some x -> x
| None -> fail "failure: assoc"
Meta.Interface.fst.checked
prims.fst.checked Meta.Attribute.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.fst.checked FStar.String.fsti.checked FStar.Reflection.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.Pure.fst.checked FStar.List.fst.checked
Meta.Interface.fst
Prims.eqtype Prims.list FStar.Pervasives.Native.tuple2 FStar.List.Tot.Base.assoc FStar.Tactics.V1.Derived.fail
module Meta.Interface

open FStar.List.Tot
open FStar.Reflection
open FStar.Tactics

/// Local library
/// -------------
val assoc (#a: eqtype) (#b: _) (x: a) (l: list (a & b)) : Tac b
x: a -> l: Prims.list (a * b) -> FStar.Tactics.Effect.Tac b