Merge pull request #19 from lean-dojo/dev

minor change
lean-dojo · Nov 12, 2023 · 8f926b0 · 8f926b0
2 parents 9d6f4c1 + 852465b
commit 8f926b0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/LeanInfer/Basic.lean b/LeanInfer/Basic.lean
@@ -65,7 +65,7 @@ def generate (input : String) (targetPrefix : String) : m (Array (String × Floa
     let temperature := config.decoding.temperature
     let beamSize := config.decoding.beamSize
     let rawOutputs := FFI.onnxGenerate input numReturnSequences maxLength temperature beamSize
-    rawOutputs.filter (λ (entry : String × Float) => entry.fst ≠ "aesop")
+    rawOutputs.filter fun (entry : String × Float) => entry.fst ≠ "aesop"
   | .native (.ct2 _) =>
     let inputTokens := tokenizeByt5 input true |>.toArray
     let targetPrefixTokens := tokenizeByt5 targetPrefix false |>.toArray