issues
search
JamesGallicchio
/
LeanColls
WIP collections library for Lean 4
https://jamesgallicchio.github.io/LeanColls/docs/
Apache License 2.0
30
stars
7
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
bump toolchain to v4.9.0
#38
JamesGallicchio
closed
2 months ago
0
Updated to lean 4.8.0-rc1
#37
mdgeorge4153
closed
3 months ago
1
Add `UInt*` byte seq instances
#36
JamesGallicchio
opened
4 months ago
0
Add String implementations
#35
JamesGallicchio
opened
4 months ago
0
Add ofFnM
#34
JamesGallicchio
opened
4 months ago
0
`Seq` on `List` is simp
#33
JamesGallicchio
closed
4 months ago
1
feat: better Dict interface
#32
JamesGallicchio
closed
4 months ago
0
chore: rename Map -> Dict
#31
JamesGallicchio
closed
4 months ago
0
Refactor operations
#30
JamesGallicchio
opened
4 months ago
1
Split LeanColls/Classes/Ops.lean
#29
JamesGallicchio
opened
4 months ago
0
bump to leanprover/lean4:v4.7.0
#28
digama0
closed
4 months ago
4
`Index.card` has an extra universe parameter
#27
JamesGallicchio
opened
5 months ago
0
feat: polymorphic range
#26
JamesGallicchio
opened
5 months ago
0
Map operation class
#25
JamesGallicchio
opened
5 months ago
3
feat: add Fold.ToList to lawfulness for Seq and IndexType
#24
JamesGallicchio
closed
5 months ago
0
GPL -> Apache
#23
JamesGallicchio
closed
6 months ago
3
Elab issues with index notation
#22
lecopivo
opened
6 months ago
1
fix: fix IndexType instances for Prod and Sum
#21
lecopivo
closed
6 months ago
0
fix: delay elaboration of index notation until types are known
#20
lecopivo
closed
6 months ago
2
Index notation cause internal exception
#19
lecopivo
closed
6 months ago
0
universe fix in `Fold`
#18
lecopivo
closed
6 months ago
1
Bump to leanprover/lean4:v4.6.0
#17
T-Brick
closed
6 months ago
0
Bump to leanprover/lean4:v4.6.0-rc1
#16
T-Brick
closed
6 months ago
1
feat: LawfulSeq instances for scalar arrays
#15
JamesGallicchio
opened
6 months ago
0
feat: Seq instances for scalar arrays
#14
JamesGallicchio
closed
6 months ago
0
feat: proofs of Fold.any/all/mem correct
#13
JamesGallicchio
closed
6 months ago
0
Fin n is LawfulIndexType
#12
lecopivo
closed
6 months ago
0
fix(ci): bump-mathlib-nightly use PAT to trigger builds
#11
JamesGallicchio
closed
6 months ago
0
Split Indexed.get_set into two cases
#10
JamesGallicchio
closed
6 months ago
1
fix: removed unecessary `DecidableEq ι` from `LawfulIndexed`
#9
lecopivo
closed
6 months ago
2
Bump to leanprover/lean4:v4.5.0
#8
T-Brick
closed
7 months ago
5
fix: fixed unresolved universe mvars in `x[i,j,k]`
#7
lecopivo
closed
7 months ago
0
feat: `x[i,j,k]` and `x[i,j,k] := xi` notation for Indexed
#6
lecopivo
closed
7 months ago
0
Add nonempty list
#5
T-Brick
closed
7 months ago
0
`reduce` and family
#4
JamesGallicchio
opened
7 months ago
2
chore: standardize container idents to `cont`
#3
JamesGallicchio
closed
7 months ago
0
Dependently typed `Indexed`
#2
lecopivo
opened
7 months ago
2
Naming arguments of Ops
#1
lecopivo
closed
7 months ago
1