Tonic commited on
Commit
7bd644e
Β·
unverified Β·
1 Parent(s): b8790bd

remove lean4 from gradio block declaration, replace with python

Browse files
Files changed (1) hide show
  1. app.py +1 -1
app.py CHANGED
@@ -183,7 +183,7 @@ def main():
183
  submit = gr.Button("Send")
184
  with gr.Column():
185
  json_out = gr.JSON(label="Full Output")
186
- code_out = gr.Code(label="Extracted Lean4 Code", language="lean4")
187
  state = gr.State([])
188
  # On submit, call chat_handler
189
  submit.click(chat_handler, [user_input, informal, max_tokens, state], [chat, json_out, code_out, state])
 
183
  submit = gr.Button("Send")
184
  with gr.Column():
185
  json_out = gr.JSON(label="Full Output")
186
+ code_out = gr.Code(label="Extracted Lean4 Code", language="python")
187
  state = gr.State([])
188
  # On submit, call chat_handler
189
  submit.click(chat_handler, [user_input, informal, max_tokens, state], [chat, json_out, code_out, state])