search

siddhartha-gadgil / LeanAide

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

Fixed some punctuations in MathDoc and ocr rules #39

Closed AnirudhG07 closed 1 month ago

AnirudhG07 commented 1 month ago

I have fixed few punctuations like, \w Give a Json list to \w. Give a Json list. and added "with the key as one of let, assume"

Also I have a suggestion, for error statements, we can write - A descriptive error in a proof or calculation. . .. In my previous reviews, many of the errors were not at all descriptive and hard to understand.

siddhartha-gadgil commented 1 month ago

This is a code generated file. Can you make the changes upstream and MathDoc.lean.

AnirudhG07 commented 1 month ago

Also I have added some rules in the OCR based on my reviews. Please review them and suggest changes. (any import position changes or addition of extra lines have been done by my vim "formatter").

AnirudhG07 commented 1 month ago

This is a code generated file. Can you make the changes upstream and MathDoc.lean.

In the MathDoc.Lean, you have used 

let body := description ++ s!" Give a JSON list, with each ...

This suggests that you do not want a full stop before Give. However previously, MathDoc.md contained both with and without a full stop. Does a . matter?

siddhartha-gadgil commented 1 month ago

The description should end with a ".".

On Fri, 18 Oct 2024 at 10:45, Anirudh Gupta @.***> wrote:

This is a code generated file. Can you make the changes upstream and MathDoc.lean.

In the MathDoc.Lean, you have used

let body := description ++ s!" Give a JSON list, with each ...

This suggests that you do not want a full stop before Give. However previously, MathDoc.md contained both with and without a full stop. Does a . matter?

— Reply to this email directly, view it on GitHub https://github.com/siddhartha-gadgil/LeanAide/pull/39#issuecomment-2421403460, or unsubscribe https://github.com/notifications/unsubscribe-auth/AA3K3JARKWOWKQBPNAW4WQTZ4CKPDAVCNFSM6AAAAABQFEHPXOVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDIMRRGQYDGNBWGA . You are receiving this because you commented.Message ID: @.***>