diff --git a/LeanCopilot/Models/ByT5.lean b/LeanCopilot/Models/ByT5.lean index f1cb513..84117ce 100644 --- 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 := ""