Issues
- 2
`lake` should give a warning when it looks like nothing is imported, by accident
#4105 opened by semorrison - 1
- 0
- 1
`lake update` should print a warning, if moving dependencies to a later toolchain than the local toolchain
#4103 opened by semorrison - 0
`Nat.zero_or` and `Nat.or_zero` are swapped
#4093 opened by fgdorais - 0
No reset/reuse instructions for simple conversion function
#4089 opened by TwoFX - 0
Lake fails to parse result of config translation script
#4099 opened by wupr - 0
`simpa` type mismatch error message could be improved
#4101 opened by kmill - 3
Renaming a variable also renames another variable
#4081 opened by mik-jozef - 0
RFC: let `unfold` tactic zeta reduce local definitions
#4090 opened by kmill - 2
Refactoring elab exception handling
#4079 opened by Kha - 0
elab_as_elim does not support function application in resulting motive arguments
#4086 opened by JamesGallicchio - 5
- 1
`And.left` and `And.right` have malformed constant info
#4064 opened by fgdorais - 3
RFC: simp control over recursive functions (or lemmas)
#4027 opened by nomeata - 4
Elaboration of explicit term proof significantly slower than equivalent tactic proof
#4051 opened by somombo - 0
Rpc Error when hovering variable
#4078 opened by hargoniX - 5
- 1
- 0
wrong `rfl` error message when no goals are left
#4063 opened by chrisflav - 24
Create a standard GitHub action for Lean projects
#3950 opened by semorrison - 2
`rw?` regression from `v4.7.0`
#4062 opened by Seasawher - 1
Hashes for `Expr.lam` and `Expr.forallE` are the same
#4060 opened by kmill - 0
lake puts relative paths in `LD_LIBRARY_PATH`
#4042 opened by eric-wieser - 0
`set_option trace.compiler.ffi_accessors`
#4041 opened by digama0 - 14
Nix builds have empty githash
#4015 opened by enricozb - 4
RFC: consistent (fine-grained?) equational lemmas
#3983 opened by nomeata - 0
- 0
error message of `register_label_attr`
#4011 opened by Seasawher - 2
`match_expr`'s parser catches semantic errors too early.
#3989 opened by hargoniX - 2
Parsing errors should be more clearly described as such.
#3990 opened by hargoniX - 1
Instance search continues even when an instance was found after a later instance could not be found
#3996 opened by MichaelStollBayreuth - 0
rewrite and instance fails
#4000 opened by craff - 0
Redundant `=?=` in elabTermEnsuringType
#3993 opened by nomeata - 3
`isDefEq` unfolds recursive definition
#3988 opened by nomeata - 2
`lake update` fails in new project with mathlib dependency (No such file or directory)
#3987 opened by rj00a - 0
simp's dischargeUsingAssumption? is not simp-cache-safe
#3943 opened by nomeata - 1
"bad" simp lemmas can lead to `acyclic` tactic failure with `simp` recursion limit
#3907 opened by fpfu - 3
Configuration option for `synthPendingDepth`
#3927 opened by mattrobball - 0
Interaction with `symm` attribute makes `apply?` nearly unusable
#3922 opened by MichaelStollBayreuth - 1
Call hierarchy and recursion
#3945 opened by nomeata - 0
Widgets not displaying on some terms
#3956 opened by Vtec234 - 1
term info missing in type ascriptions in patterns
#3955 opened by digama0 - 0
Speed up interactivetests
#3941 opened by Kha - 3
RFC: discoverability of linter options
#3937 opened by hargoniX - 0
Timeout on large pattern matches against Nat
#3935 opened by gleachkr - 1
question: why wait for `initialized` is needed here?
#3904 opened by alissa-tung - 2
RFC: `termination_by structurally x`
#3909 opened by nomeata - 2
GuessLex too clever for the default terminaton_tactic.
#3906 opened by nomeata - 1