kaiyuy
/

leandojo-lean3-tacgen-byt5-small

text2text-generation

text-generation-inference

Model card Files Files and versions

kaiyuy commited on Jun 23, 2023

Commit

74546ca

·

1 Parent(s): 0a5cfdb

Update README.md

Files changed (1) hide show

README.md +6 -0

README.md CHANGED Viewed

@@ -1,5 +1,11 @@
 ---
 license: mit
 ---
 [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://arxiv.org/abs/xxxx.xxxxx)

 ---
 license: mit
+inference:
+  parameters:
+    max_length: 1024
+widget:
+- text: "a b c : ℕ\n⊢ a + b + c = a + c + b"
+  example_title: "Example"
 ---
 [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://arxiv.org/abs/xxxx.xxxxx)