From aa1c4a311cacb1b083667eb0c7151ac3d00efd9b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= <theophile@wallez.net>
Date: Wed, 27 Nov 2024 15:26:14 +0100
Subject: [PATCH] cleanup: remove lambda in TreeSyncTreeKEMBinder

---
 fstar/glue/code/MLS.TreeSyncTreeKEMBinder.fst | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/fstar/glue/code/MLS.TreeSyncTreeKEMBinder.fst b/fstar/glue/code/MLS.TreeSyncTreeKEMBinder.fst
index 503cab5..a377eb4 100644
--- a/fstar/glue/code/MLS.TreeSyncTreeKEMBinder.fst
+++ b/fstar/glue/code/MLS.TreeSyncTreeKEMBinder.fst
@@ -11,6 +11,9 @@ open MLS.Result
 
 #set-options "--fuel 1 --ifuel 1"
 
+val nat_lbytes_to_nat: #sz:nat -> nat_lbytes sz -> nat
+let nat_lbytes_to_nat #sz x = x
+
 val treesync_to_treekem_node:
   #bytes:Type0 -> {|crypto_bytes bytes|} ->
   parent_node_nt bytes tkt ->
@@ -18,7 +21,7 @@ val treesync_to_treekem_node:
 let treesync_to_treekem_node #bytes #cb node =
   {
     public_key = node.content;
-    unmerged_leaves = List.Tot.map #(nat_lbytes 4) #nat (fun x -> x) node.unmerged_leaves;
+    unmerged_leaves = List.Tot.map nat_lbytes_to_nat node.unmerged_leaves;
   }
 
 // This does not contain any internal TreeKEM data. To be used then joining a new group.