search

siddhartha-gadgil / LeanAide

Tools based on AI for helping with Lean 4
Apache License 2.0
65 stars 5 forks source link

Re structure enhancements #21

Closed 0art0 closed 1 year ago

0art0 commented 1 year ago

An abstract configuration for the interface is ready (and can be experimented with in the StatementAutoformalisation/Experiment file). This pull request will include an interface for autoformalisation (for which the main barrier is finding the nearest theorem/def to the cursor position) and keyword-based prompting.

0art0 commented 1 year ago

Code actions for informalisation are now available.