New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add MIL.Common import to intro example #278

Open

gaearon wants to merge 1 commit into avigad:master from gaearon:patch-1

gaearon commented Feb 1, 2025

I started reading MIL and was confused by the very first example not working.

Screenshot 2025-02-01 at 20 34 33

I pasted this into the Lean file but got this:

Screenshot 2025-02-01 at 20 35 34

Not saying this is the best possible fix pedagogically...

A few alternative suggestions:

Could avoid using the shortcut notation until the next chapter
Could add import MIL.Common to S01_Getting_Started.lean in the project repo instead to give a hint


          Add MIL.Common import to intro example

37ec1fb

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet