val opt_list_to_list_or_empty (#a: Type) (ols: option (list a)) : list a
val opt_list_to_list_or_empty (#a: Type) (ols: option (list a)) : list a
let opt_list_to_list_or_empty (#a : Type) (ols : option (list a)) : list a =
  match ols with
  | Some ls -> ls
  | None -> []
module Spec.Noise.HandshakeFlags
open FStar.Mul

open Spec.Noise.CryptoPrimitives
open Spec.Noise.Base

/// The following file implements functions, predicates and lemmas to reason about
/// the availability of the different keys in the handshake (and cipher) state at
/// every step of the handshake. On top of that it also builds pattern
/// well-formedness analysis.

#set-options "--z3rlimit 15 --fuel 0 --ifuel 1"
/
Spec.Noise.CryptoPrimitives.fsti.checked Spec.Noise.Base.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked
Spec.Noise.HandshakeFlags.fsti
ols: FStar.Pervasives.Native.option (Prims.list a) -> Prims.list a
FStar.Pervasives.Native.option Prims.list Prims.Nil
let opt_list_to_list_or_empty (#a: Type) (ols: option (list a)) : list a =
  
match ols with
| Some ls -> ls
| None -> []