Repository navigation

All pull requests

Labels (13)Milestones (0)New pull request

feat: support ← for simp rules
#362josaum opened Oct 25, 2026
fix: preserve simprocs when erasing rules
#361CollinYuanjieRen opened Oct 16, 2026
Preserve injectivity when comparing renamed expression goals
#356chessing234 opened Oct 5, 2026
fix: require injective universe metavariable renaming
#354chessing234 opened Oct 1, 2026
perf: cluster shared features through one representative
#353chessing234 opened Oct 1, 2026
fix: format nanosecond durations using integer arithmetic
#352chessing234 opened Oct 1, 2026
fix: warn/error on forward and destruct rules with no slots
#347chessing234 opened Sep 16, 20262 tasks done
fix: UnionFind.add pushes size onto sizes
#338chessing234 opened Jul 17, 20261 task
fix: correctly identify pattern substitutions
#335ericluap opened Jun 26, 2026
build(deps): bump actions/checkout from 6 to 7
#334dependabot[bot] opened Jun 19, 2026Bot
fix: Invalid field lDepth
#326srghma opened Apr 21, 2026
chore: adapt to new do elaborator
#323sgraf812 opened Apr 16, 2026
Fix a typo in README
#313pevogam opened Feb 26, 2026
2
adaptation for leanprover/lean#11936
#303datokrat opened Jan 12, 2026
chore: add docstrings for the undocumented tactics
#281Vierkantor opened Dec 11, 2025Contributor