Skip to content

Conversation

@ineol
Copy link

@ineol ineol commented Mar 18, 2025

There is one lemma that I couldn't easily prove, because the definition of fixed width integers changed

@ineol ineol force-pushed the update-lean-2025-03-17 branch from e957e29 to f9b66dc Compare March 18, 2025 18:13
@ineol ineol marked this pull request as ready for review March 18, 2025 18:14
@gleachkr
Copy link
Collaborator

Thanks, and sorry for the slow reply. At the moment, I'd like to make sure not to diverge from https://github.com/leanprover/LNSym (unless someone over there tells me it's safe to do so), but if you notice that they've advanced their lean version, please let me know and I'll bump things on this end.

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

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants