issues
search
dselsam
/
binport
A tool for building Lean4 .olean files from Lean3 export data
Apache License 2.0
10
stars
1
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Position Info Support
#26
AurelienSaue
opened
3 years ago
1
Put in `Mathlib` namespace?
#25
dselsam
opened
3 years ago
0
error: invalid argument name 'self'
#24
dselsam
closed
2 years ago
4
Capitalization mismatch
#23
dselsam
opened
3 years ago
1
Lean4 does not support post-facto instance priority changes
#22
dselsam
opened
3 years ago
3
Instance subgoal order has changed from R->L to L->R
#21
dselsam
closed
3 years ago
2
Well-founded rfl-proofs even less likely to work in MetaM
#20
dselsam
opened
3 years ago
0
Control
#19
dselsam
closed
3 years ago
2
Strings
#18
dselsam
closed
3 years ago
6
Numbers
#17
dselsam
opened
3 years ago
4
Aligning `dite`/`ite`
#16
dselsam
closed
3 years ago
1
Aligning `Nat.le`
#15
dselsam
opened
3 years ago
1
Automatically construct `Trans` instances from relation manager exports
#14
dselsam
opened
3 years ago
0
Make sure all standard Lean4 constructions are constructed
#13
dselsam
closed
3 years ago
2
Auto-generated names need to depend on module
#12
dselsam
closed
3 years ago
3
Miscellaneous mismatches: dite, fin, unsigned, char, string, array, control structures, ...
#11
dselsam
closed
3 years ago
1
Is idDelta still necessary?
#10
dselsam
closed
3 years ago
3
Non-mixfix notation not ported
#9
dselsam
opened
3 years ago
0
Auto-port missing `noindex!` annotations
#8
dselsam
opened
3 years ago
2
No more support for irreducible or post-facto reducible-toggling
#7
dselsam
opened
3 years ago
0
Alignment not carrying over to namespaces
#6
dselsam
opened
3 years ago
0
TC now requires more universe annotations
#5
dselsam
closed
3 years ago
7
Non-struct classes are not supported
#4
dselsam
opened
3 years ago
4
No more (kernel) support for reducing inductive result types
#3
dselsam
opened
3 years ago
2
Surprising need for `noindex!` annotation
#2
dselsam
closed
3 years ago
5
Differing behavior on clashing binders
#1
dselsam
opened
3 years ago
5