val max : x: Prims.int -> y: Prims.int -> Prims.int
let max x y = if x <= y then y else x
module MiTLS.Pkg.Tree
open MiTLS

open MiTLS.Mem
open MiTLS.Pkg
open MiTLS.Idx

/// We use subtrees to specify KDF usages. We hope we can erase
/// them when modelling is off!
///
/// This module is generic, and could be made parametric in its index
/// package. The TLS-specific details are filled-in in KeySchedule.

type t = pkg ii

noeq noextract
type tree' (par_ideal:Type0) =
  | Leaf: package:t{Pkg?.ideal package ==> par_ideal} -> tree' par_ideal
  | Node: node:t{Pkg?.ideal node ==> par_ideal} -> children: children' (Pkg?.ideal node) -> tree' par_ideal
and children' (par_ideal:Type0) = list (label * tree' par_ideal)

// would prefer to use Map.t, but positivity check fails
/
prims.fst.checked MiTLS.Pkg.fst.checked MiTLS.Mem.fst.checked MiTLS.Idx.fst.checked FStar.Pervasives.fsti.checked
MiTLS.Pkg.Tree.fst
x: Prims.int -> y: Prims.int -> Prims.int
Prims.int Prims.op_LessThanOrEqual Prims.bool
let max x y =
  
if x <= y then y else x