issues
search
leanprover
/
lean4
Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
3.78k
stars
323
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
perf: issue at `binop%` and `binrel%` elaborators
#4085
leodemoura
opened
1 hour ago
1
fix: missing update stage0
#4084
leodemoura
closed
1 hour ago
1
refactor: lake: manifest semver & code cleanup
#4083
tydeu
opened
4 hours ago
1
feat: collect kernel diagnostic information
#4082
leodemoura
closed
4 hours ago
1
Renaming a variable also renames another variable
#4081
mik-jozef
opened
7 hours ago
2
fix: code duplication at `liftCoreM` and `liftTermElabM` at `Command.lean`
#4080
leodemoura
closed
6 hours ago
3
Refactoring elab exception handling
#4079
Kha
opened
10 hours ago
1
Rpc Error when hovering variable
#4078
hargoniX
opened
15 hours ago
0
chore: move @[simp] attribute on length_eq_zero earlier
#4077
semorrison
closed
14 hours ago
1
To int eq broken
#4076
tobiasgrosser
closed
18 hours ago
1
feat: add BitVec.[toInt_eq|toInt_ne]
#4075
tobiasgrosser
opened
18 hours ago
1
refactor: Array.feraseIdx: avoid have in definition
#4074
nomeata
closed
18 hours ago
3
chore: allow omega to use classicality, in case Decidable instances are too big
#4073
semorrison
closed
15 minutes ago
1
[Backport releases/v4.8.0] fix: have app unexpanders be considered before field notation
#4072
github-actions[bot]
closed
21 hours ago
1
fix: have app unexpanders be considered before field notation
#4071
kmill
closed
1 day ago
1
refactor: subst notation try to run isDefEq only once
#4070
nomeata
closed
1 day ago
1
'Building X' diagnostic for every dependency when processing imports
#4069
bustercopley
opened
1 day ago
1
[Backport releases/v4.8.0] fix: rfl tactic error messsage when there are no goals
#4068
github-actions[bot]
closed
1 day ago
0
fix: rfl tactic error messsage when there are no goals
#4067
nomeata
closed
1 day ago
1
fix: mainModuleName should use srcSearchPath
#4066
digama0
opened
2 days ago
1
fix: bug in reduceLeDiff simproc proof term
#4065
digama0
closed
1 day ago
2
`And.left` and `And.right` have malformed constant info
#4064
fgdorais
closed
1 hour ago
1
wrong `rfl` error message when no goals are left
#4063
chrisflav
closed
1 day ago
0
`rw?` regression from `v4.7.0`
#4062
Seasawher
opened
2 days ago
2
feat: well-founded definitions irreducible by default
#4061
nomeata
opened
3 days ago
4
Hashes for `Expr.lam` and `Expr.forallE` are the same
#4060
kmill
opened
3 days ago
1
feat: upstream lemmas about basic List/Array operations
#4059
semorrison
closed
22 hours ago
4
chore: begin development cycle for v4.9.0
#4058
semorrison
closed
3 days ago
1
feat: lake: `require` doc comments
#4057
tydeu
closed
4 days ago
2
chore: lake: cleanup tests
#4056
tydeu
closed
4 days ago
1
fix: remove `Subtype.instInhabited`
#4055
kmill
closed
15 hours ago
3
a case where omega used to work in 4.7.0 and doesn't work in 4.8.0-rc1
#4054
hwatheod
closed
15 minutes ago
5
feat: add `seal` and `unseal` commands
#4053
leodemoura
closed
3 days ago
6
feat: validate reducibility attribute setting
#4052
leodemoura
closed
3 days ago
1
Elaboration of explicit term proof significantly slower than equivalent tactic proof
#4051
somombo
opened
4 days ago
4
chore: CI: use large runners on Windows
#4050
Kha
closed
4 days ago
2
chore: report used instances correctly in diagnostics
#4049
semorrison
closed
4 days ago
1
feat: display diagnostic information at term and tactic `set_option diagnostics true`
#4048
leodemoura
closed
5 days ago
1
refactor: do not try rfl in mkEqnTypes in WF.mkEqns
#4047
nomeata
closed
4 days ago
4
feat: subst notation (heq ▸ h) tries both orientation
#4046
nomeata
closed
4 days ago
1
doc: mention build doc source location
#4045
kmill
closed
5 days ago
1
perf: improve `simp` cache behavior for well-behaved dischargers
#4044
leodemoura
closed
5 days ago
1
feat: include congruence theorems at `simp` diagnostic information
#4043
leodemoura
closed
5 days ago
1
lake puts relative paths in `LD_LIBRARY_PATH`
#4042
eric-wieser
opened
5 days ago
0
`set_option trace.compiler.ffi_accessors`
#4041
digama0
opened
6 days ago
0
feat: `set_option diagnostics true` for `simp`, and structured diagnostic messages
#4040
leodemoura
closed
6 days ago
1
chore: remove @[simp] from BitVec.of_length_zero
#4039
semorrison
closed
6 days ago
1
chore: restore #4006
#4038
semorrison
closed
6 days ago
1
feat: lemmas to simplify equalities with `Option`-typed dependent if-then-else
#4037
wupr
closed
20 hours ago
6
feat: `IO.Process.get/setCurrentDir`
#4036
tydeu
closed
4 days ago
1
Next