val swap_pair (#a #b: Type) (p: a & b) : b & a
val swap_pair (#a #b: Type) (p: a & b) : b & a
let swap_pair (#a #b : Type) (p : a & b) : b & a =
  match p with x, y -> y, x
module Spec.Noise.Testing.Base

open Lib.IntTypes
open Lib.RawIntTypes
open Lib.ByteSequence
open Lib.Sequence

open Spec.Noise.CryptoPrimitives
open Spec.Noise.Base
open Spec.Noise.WellFormedness
open Spec.Noise.Patterns

open Spec.Noise.Utils

open FStar.All
module IO = FStar.IO

#set-options "--z3rlimit 15 --fuel 0 --ifuel 1"

/// The following file defines testing utilities for the Noise patterns
/
Spec.Noise.WellFormedness.fsti.checked Spec.Noise.Utils.fst.checked Spec.Noise.Patterns.fst.checked Spec.Noise.CryptoPrimitives.fsti.checked Spec.Noise.Base.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.Pure.Properties.fst.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.All.fst.checked
Spec.Noise.Testing.Base.fst
p: (a * b) -> b * a
FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.Mktuple2
let swap_pair (#a #b: Type) (p: a & b) : b & a =
  
match p with | x, y -> y, x