Skip to content

Internal Eq#177

Open
markusdemedeiros wants to merge 5 commits intomasterfrom
internaleq
Open

Internal Eq#177
markusdemedeiros wants to merge 5 commits intomasterfrom
internaleq

Conversation

@markusdemedeiros
Copy link
Collaborator

Description

Internal Equality. This should really be derived from the SBI interface. I do not recommend it be merged until that is the case.

Checklist

  • My code follows the mathlib naming and code style conventions
  • I have updated PORTING.md as appropriate
  • I have added my name to the authors section of any appropriate files

@markusdemedeiros markusdemedeiros added the blocked The issue is blocked by a different issue. label Mar 18, 2026
@markusdemedeiros
Copy link
Collaborator Author

Blocked by #178

@markusdemedeiros markusdemedeiros mentioned this pull request Mar 18, 2026
3 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

blocked The issue is blocked by a different issue.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant