issues
search
leanprover-community
/
aesop
White-box automation for Lean 4
Apache License 2.0
155
stars
25
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
chore: adaptations for leanprover/lean4#3040 (changes to termination hints)
#95
semorrison
closed
5 months ago
1
Aesop ruleset runs forever
#94
adomasbaliuka
opened
6 months ago
1
chore: adaptations for leanprover/lean4#3124
#93
semorrison
closed
5 months ago
0
chore: adjust to lean4#3123
#92
nomeata
closed
6 months ago
1
chore: move toolchain to v4.5.0-rc1
#91
semorrison
closed
6 months ago
0
chore: move toolchain to v4.4.0
#90
semorrison
closed
6 months ago
0
`aesop?` suggests unusable `_private.Mathlib.Data.Set.Pointwise.Basic.0.Set.involutiveNeg._eq_1`
#89
adomasbaliuka
opened
7 months ago
2
chore: bump toolchain to v4.4.0-rc1
#88
semorrison
closed
7 months ago
0
chore: bump toolchain to v4.3.0
#87
semorrison
closed
7 months ago
0
chore: fix imports
#86
fgdorais
closed
7 months ago
1
RFC: fail if no rules are applied
#85
semorrison
closed
7 months ago
1
chore: bump Std dependency
#84
semorrison
closed
8 months ago
0
chore: bump toolchain to v4.3.0-rc1
#83
semorrison
closed
8 months ago
0
chore: bump toolchain to v4.2.0
#82
semorrison
closed
8 months ago
0
chore: adaptations for leanprover/lean4#2714
#81
semorrison
closed
7 months ago
5
Update README.md `trace.aesop.finalTree` => `trace.aesop.tree`
#80
adomasbaliuka
closed
8 months ago
1
chore: update for changes to DiscrTree in leanprover/lean4#2734
#79
semorrison
closed
7 months ago
1
chore: adapt to `decide := false` in simp
#78
collares
closed
8 months ago
3
chore: bump toolchain to v4.2.0-rc4
#77
semorrison
closed
8 months ago
0
`simp_all` May Make Goals Unprovable
#76
yangky11
closed
8 months ago
2
chore: bump toolchain to v4.2.0-rc3
#75
semorrison
closed
8 months ago
0
traceScript is ignored when the maximum rule application depth is reached
#74
semorrison
closed
8 months ago
1
Set intros transparency via a ruleset, rather than an option?
#73
semorrison
opened
8 months ago
2
chore: bump to v4.2.0-rc2
#72
semorrison
closed
8 months ago
0
fix: use replay from leanprover/lean4#2617
#71
semorrison
closed
8 months ago
2
Add New Rule Builder: Tactic Generator
#70
yangky11
closed
9 months ago
6
Refactor
#69
yangky11
closed
9 months ago
1
refactor: Adjust to new DiscrTree implementation
#68
nomeata
closed
6 months ago
0
chore: update to v4.0.0-rc4
#67
semorrison
closed
10 months ago
2
chore: update to v4.0.0-rc3
#66
semorrison
closed
10 months ago
1
chore: bump to nightly-2023-08-19
#65
semorrison
closed
10 months ago
1
chore: bump to nightly-2023-08-16
#64
semorrison
closed
10 months ago
2
Use `Std.Tactic.TryThis` API
#63
JLimperg
closed
10 months ago
0
Simp builder silently ignores rule penalty
#62
JLimperg
closed
10 months ago
1
Phase must be specified when using simp builder
#61
JLimperg
closed
10 months ago
0
Doc clarification on forward rules with no immediates
#60
ammkrn
closed
1 year ago
1
aesop ignores @[eliminator]
#59
semorrison
opened
1 year ago
1
`aesop` has no doc string
#58
digama0
closed
1 year ago
0
Consider not using checkpointing
#57
ocfnash
closed
1 year ago
2
Fix spacing in grammar
#56
digama0
closed
1 year ago
1
Consider excluding obviously-looping local equations from the norm simp call
#55
JLimperg
opened
1 year ago
2
Builtin rules loop on simple goal with negation
#54
JLimperg
opened
1 year ago
0
Update README.md
#53
BoltonBailey
closed
1 year ago
1
`lake build` failed
#52
yangky11
closed
1 year ago
2
Add profiling metric for Aesop
#51
JLimperg
closed
1 year ago
0
Support safe/unsafe rules in `unfold` builder
#50
JLimperg
opened
1 year ago
0
Use collapsible `MessageData` for tracing
#49
JLimperg
closed
1 year ago
0
Move Aesop.Test into a separate library.
#48
gebner
closed
1 year ago
1
Print goal when Aesop fails with `terminal := true`
#47
JLimperg
closed
1 year ago
0
`cases` builder should accept type synonyms
#46
JLimperg
closed
1 year ago
1
Previous
Next