issues
search
leanprover-community
/
lean-auto
Experiments in automation for Lean
Apache License 2.0
73
stars
12
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
LamTerm.betaBounded bug
#38
JOSHCLUNE
opened
2 weeks ago
0
Issue with auto.native
#37
threonorm
opened
3 weeks ago
0
fix trace bugs
#36
JOSHCLUNE
closed
1 month ago
0
Delete profile messages.
#35
abdoo8080
opened
1 month ago
0
change interface signature
#34
JOSHCLUNE
closed
1 month ago
0
fix leadingForallQuasiMonomorphic bug
#33
JOSHCLUNE
closed
1 month ago
0
Merge main into duper2
#32
JOSHCLUNE
closed
1 month ago
0
Update to v4.11.0
#31
JOSHCLUNE
closed
2 months ago
1
Any better way to work around `Higher order input?` error in the SMT mode?
#30
zqy1018
opened
2 months ago
0
Sexp parser seemingly broken in update from Lean 4.9 to 4.11
#29
ymherklotz
closed
1 month ago
1
Fix CVC5 model comments
#28
dranov
closed
4 months ago
0
Bump toolchain to v4.8.0
#27
dranov
closed
5 months ago
0
SMT names that match Lean names
#26
dranov
closed
6 months ago
11
bump to 4.8.0-rc1
#25
AdrienChampion
closed
5 months ago
3
Add support for SMT triggers
#24
atomb
closed
7 months ago
0
Change lexer to ignore comments
#23
dranov
closed
7 months ago
0
Lean Auto fails to translate some type classes
#22
volodeyka
closed
7 months ago
0
automate test suite
#21
kim-em
opened
9 months ago
0
Merge updated DTr data structure so Duper can track isFromGoal information
#20
JOSHCLUNE
closed
9 months ago
0
adaptations required for nightly-2024-02-18
#19
kim-em
closed
8 months ago
0
Fix string-format in warning for inductive types
#18
dranov
closed
9 months ago
1
feat: bump Std
#17
kim-em
closed
9 months ago
0
Fix existentially quantified `Nat`s
#16
dranov
closed
9 months ago
0
Faulty translation of `Nat` existentials into SMT
#15
dranov
closed
9 months ago
0
TPTP Parser Bug Fix
#14
JOSHCLUNE
closed
9 months ago
0
Improve README
#13
DenisGorbachev
closed
10 months ago
1
Feature Request: Allow users to map suitable Lean functions to corresponding SMT functions
#12
shigoel
opened
10 months ago
0
Zero-width bitvectors
#11
shigoel
opened
11 months ago
0
LT and LE for bitvectors
#10
shigoel
closed
10 months ago
3
Feature request: configuration option to write generated SMT commands to a file instead of being displayed on stdout
#9
shigoel
closed
11 months ago
4
Feature request: configuration option to allow the user to change solver timeouts
#8
shigoel
closed
11 months ago
2
Feature request: define SMT functions that match Lean names whenever possible for ease of debugging & readability
#7
shigoel
opened
11 months ago
3
Bug in the translation of `Std.BitVec.not`
#6
shigoel
closed
11 months ago
2
Feature requests: Meaningful UNSAT cores and Models in Lean
#5
mww-aws
opened
1 year ago
3
lean-auto failure on simple model.
#4
mww-aws
opened
1 year ago
4
Feature request: SMT trigger annotations
#3
atomb
closed
7 months ago
0
Modifying monoPrepInterface signature
#2
JOSHCLUNE
closed
1 year ago
1
chore: bump lean-toolchain to v4.2.0-rc4
#1
kim-em
closed
1 year ago
0