issues
search
leanprover-community
/
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Apache License 2.0
250
stars
104
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
feat: more vector lemmas
#1062
fgdorais
opened
2 hours ago
2
chore: fix two deprecations
#1061
kim-em
closed
2 hours ago
1
chore: test
#1060
fgdorais
closed
10 hours ago
0
chore: fix workflow token
#1059
fgdorais
closed
10 hours ago
1
chore: adaptations for nightly-2024-11-20
#1058
kim-em
opened
2 days ago
0
chore: cleanup breaking non-terminal simps
#1057
kim-em
closed
2 days ago
1
fix: Readme.md needs "git" token in lakefile.lean
#1056
JaredCorduan
closed
1 day ago
2
refactor: add List.finRange and Array.finRange
#1055
fgdorais
opened
4 days ago
2
chore: remove @[simp] attributes from monad-specific SatisfiesM lemmas
#1054
kim-em
closed
4 days ago
2
chore: adaptations for nightly-2024-11-18
#1053
kim-em
closed
2 days ago
0
refactor: define `List.IsChain`, deprecate `Chain` and `Chain'`
#1052
urkud
opened
6 days ago
8
chore: adjust workflow permissions
#1051
fgdorais
closed
1 week ago
1
fix: use two tokens for open private/export private
#1050
david-christiansen
closed
1 week ago
4
chore: adaptations for nightly-2024-11-14
#1049
kim-em
closed
5 days ago
0
chore: adaptations for nightly-2024-11-13
#1048
kim-em
closed
1 week ago
0
fix: run `Lean.enableInitializersExecution`
#1047
eric-wieser
closed
1 week ago
1
chore: deprecate Expr.forallArity, per todo
#1046
kim-em
closed
1 week ago
2
chore: update authors lines
#1045
kim-em
closed
1 week ago
1
chore: remove >6 month old deprecations
#1044
kim-em
closed
1 week ago
2
chore: remove duplicate NameMap forIn instance
#1043
kim-em
closed
1 week ago
1
chore: remove unnecessary import in Batteries.Lean.LawfulMonad
#1042
kim-em
closed
1 week ago
1
chore: reset to `nightly-testing`
#1041
thorimur
closed
1 week ago
1
chore: adaptations for nightly-2024-11-12
#1040
kim-em
closed
1 week ago
0
chore: cleanup proof of satisfiesM_foldlM
#1039
kim-em
closed
1 week ago
1
chore: robustify some String proofs
#1038
kim-em
closed
1 week ago
1
fix: add missing `initHeartbeats`
#1037
eric-wieser
opened
1 week ago
2
perf: inline the `Decidable (Coprime _ _)` instance
#1036
eric-wieser
closed
1 week ago
1
chore(Data/Rat): move Float functions to separate file
#1035
jcommelin
closed
1 week ago
1
feat: List.SatisfiesM_foldlM
#1034
kim-em
closed
1 week ago
2
chore: add unlabeled PR workflow
#1033
fgdorais
closed
1 week ago
1
"Internalizing" external reasoning about monadic actions (`SatisfiesM`)
#1032
Ericson2314
closed
1 week ago
2
chore: update README with new lakefile syntax
#1031
fgdorais
closed
1 week ago
1
feat: improve induction code action
#1030
digama0
closed
1 week ago
3
feat: sugar for SatisfiesM
#1029
kim-em
closed
1 week ago
17
feat: generate docs from subdirectory
#1028
fgdorais
closed
1 week ago
2
chore: adaptations for nightly-2024-11-07
#1027
kim-em
closed
1 week ago
1
feat: Vector.mapM
#1026
kim-em
closed
1 day ago
1
refactor: cleanup `Vector` API
#1025
fgdorais
closed
1 week ago
1
chore: turn batteries tests into a library
#1024
edegeltje
closed
2 weeks ago
1
chore: move toolchain to v4.14.0-rc1
#1023
kim-em
closed
2 weeks ago
0
chore: adaptations for nightly-2024-11-01
#1022
kim-em
closed
2 weeks ago
0
chore: bump toolchain to v4.13.0
#1021
kim-em
closed
3 weeks ago
1
chore: adaptations for nightly-2024-10-18 thru 2024-10-30
#1020
kim-em
closed
3 weeks ago
0
fix: ignore comments in `#where`
#1019
adomani
closed
3 weeks ago
3
feat: fill some gaps in Vector lemmas
#1018
kim-em
closed
3 weeks ago
1
fix: github script fix head repo
#1017
fgdorais
closed
3 weeks ago
0
fix: github script typo
#1016
fgdorais
closed
3 weeks ago
0
fix: github script use list instead of view
#1015
fgdorais
closed
3 weeks ago
0
fix: github script another typo
#1014
fgdorais
closed
3 weeks ago
0
fix: github script fix repo again
#1013
fgdorais
closed
3 weeks ago
0
Next