val compatible : k: Zeta.GenKey.key aprm -> v: Zeta.Record.value aprm -> Prims.bool
let compatible #aprm (k: key aprm) (v: value aprm) =
  match k, v with
  | AppK _, AppV _ -> true
  | IntK _, IntV _ -> true
  | AppK _, IntV _ -> false
  | IntK _, AppV _ -> false
module Zeta.Record

open FStar.BitVector
open Zeta.App
open Zeta.BinTree
open Zeta.Hash
open Zeta.Merkle
open Zeta.GenKey

type value (aprm: app_params) =
  | AppV: v: app_value_nullable aprm.adm -> value aprm
  | IntV: v: Merkle.value -> value aprm
/
Zeta.Merkle.fsti.checked Zeta.Hash.fsti.checked Zeta.GenKey.fsti.checked Zeta.BinTree.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.BitVector.fst.checked
Zeta.Record.fsti
k: Zeta.GenKey.key aprm -> v: Zeta.Record.value aprm -> Prims.bool
Zeta.App.app_params Zeta.GenKey.key Zeta.Record.value FStar.Pervasives.Native.Mktuple2 Zeta.App.app_key Zeta.App.__proj__Mkapp_params__item__adm Zeta.App.app_value_nullable Zeta.Key.merkle_key Zeta.Merkle.value Prims.bool
let compatible #aprm (k: key aprm) (v: value aprm) =
  
match k, v with
| AppK _, AppV _ -> true
| IntK _, IntV _ -> true
| AppK _, IntV _ -> false
| IntK _, AppV _ -> false