val synth_pairs_to_struct_to_pairs_tac
      (#struct_t #pairs_t: Type)
      (recip: (struct_t -> GTot pairs_t))
      (n: nat)
    : Tac unit
let synth_pairs_to_struct_to_pairs_tac (#struct_t: Type) (#pairs_t: Type) (recip: struct_t -> GTot pairs_t) (n: nat) : Tac unit =
  apply (quote (synth_inverse_synth_injective' recip));
  synth_pairs_to_struct_to_pairs_tac' n
val synth_pairs_to_struct_to_pairs_tac
      (#struct_t #pairs_t: Type)
      (recip: (struct_t -> GTot pairs_t))
      (n: nat)
    : Tac unit
let synth_pairs_to_struct_to_pairs_tac
      (#struct_t #pairs_t: Type)
      (recip: (struct_t -> GTot pairs_t))
      (n: nat)
    : Tac unit =
apply (quote (synth_inverse_synth_injective' recip));
synth_pairs_to_struct_to_pairs_tac' n
LowParse.Spec.Tac.Combinators.fst.checked
prims.fst.checked LowParse.TacLib.fst.checked LowParse.Spec.Combinators.fsti.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked
LowParse.Spec.Tac.Combinators.fst
Prims.nat LowParse.Spec.Tac.Combinators.synth_pairs_to_struct_to_pairs_tac' Prims.unit FStar.Tactics.V1.Derived.apply FStar.Reflection.Types.term LowParse.Spec.Combinators.synth_inverse_synth_injective'
module LowParse.Spec.Tac.Combinators
include LowParse.Spec.Combinators

open LowParse.TacLib

(* for structs *)

let rec destruct_lhs_pairs (t: FStar.Tactics.term) (n: nat) : FStar.Tactics.Tac unit =
  if n = 0
  then trefl ()
  else begin
    destruct t;
    let a = intro () in
    let b = intro () in
    let abeq = intro () in
    rewrite abeq;
    destruct_lhs_pairs (binder_to_term a) (n - 1)
  end

let synth_pairs_to_struct_to_pairs_tac' (n: nat) : Tac unit =
  norm [delta]; // _only [(`%synth_inverse); (`%t8')]];
  let x = forall_intro () in
  destruct_lhs_pairs (binder_to_term x) n
val synth_pairs_to_struct_to_pairs_tac
      (#struct_t #pairs_t: Type)
      (recip: (struct_t -> GTot pairs_t))
      (n: nat)
    : Tac unit
recip: (_: struct_t -> Prims.GTot pairs_t) -> n: Prims.nat -> FStar.Tactics.Effect.Tac Prims.unit