Fix string UTF-8 misformatting PANIC

lean-dojo · Aug 14, 2024 · 7e4910c · 7e4910c
1 parent d7ad9f5
commit 7e4910c
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/LeanCopilot/Models/ByT5.lean b/LeanCopilot/Models/ByT5.lean
@@ -281,7 +281,9 @@ def tokenize (text : String) : Array String :=
 
 
 def detokenize (tokens : Array String) : String :=
-  String.fromUTF8! ⟨tokens.map tokenToByte!⟩
+  match (String.fromUTF8? ⟨tokens.map tokenToByte!⟩) with
+  | some s => s
+  | none => ""
 
 
 def eosToken := "</s>"