leanprover/lean4

Issues

• No docstring is show on `·` terms

  #5737 opened 2 months ago by eric-wieser
  0

• No progress indicator for a long time when downloading a project in VSCode

  #5615 opened 3 months ago by kim-em
  2

• clear does not work in `conv` mode

  #5734 opened 2 months ago by bollu
  3

• kernel hangs on ac_nf expression

  #5699 opened 2 months ago by tobiasgrosser
  4

• omega does not look through abbreviations in types

  #5733 opened 2 months ago by nomeata
  0

• `PANIC at outOfBounds` on theorem involving a nested inductive

  #5726 opened 2 months ago by ionathanch
  0

• Deep kernel reduction detected after `simp`

  #5724 opened 2 months ago by tobiasgrosser
  0

• Metavariable instantiation seems to slow down non-linearly in the size of the proof

  #5610 opened 3 months ago by alexkeizer
  2

• simp usually reduces `Fin n` literals, but not `n` itself

  #5630 opened 2 months ago by nomeata
  0

• rcases doesn't complain about unsynthesized placeholder

  #5723 opened 2 months ago by fpvandoorn
  0

• `show_term` and `by?` change order of elaboration

  #5713 opened 2 months ago by kmill
  0

• Slow elaboration of `List Nat` literals

  #5683 opened 2 months ago by kmill
  3

• Unable to figure the term when destructing an inductive proposition

  #5700 opened 2 months ago by fduxiao
  2

• Application type mismatch in simp involving dsimp theorem

  #5702 opened 2 months ago by JLimperg
  0

• Universe level normalization has associativity of `max` backwards from parsing associativity

  #5695 opened 2 months ago by kmill
  0

• RFC: decide! tactic variant

  #5629 opened 2 months ago by nomeata
  6

• Recursive theorems with `cases` vs `match`

  #5690 opened 2 months ago by hargoniX
  2

• "-f" flag not recognized as alternative to "--features"

  #5682 opened 2 months ago by James-Oswald
  1

• Structure eta doesn't work for nested inductives

  #5661 opened 3 months ago by nomeata
  12

• `bv_decide` throws an `unknown free variable` error if there is an hypothesis `b.toNat > 0` in the context

  #5674 opened 2 months ago by alexkeizer
  0

• Instance creates defs regardless of whether the typeclass is Prop- or Type-valued

  #5672 opened 2 months ago by jjdishere
  0

• "failed to generate equational theorem" when matching on not only recursive call

  #5667 opened 3 months ago by nomeata
  5

• bug: `bv_decide` regression; proof that worked before now times out, and LRAT file sizes are much larger

  #5664 opened 2 months ago by alexkeizer
  3

• `<|>` notation is not pretty-printed

  #5668 opened 3 months ago by TwoFX
  0

• `rintro` error message is in the wrong place

  #5659 opened 3 months ago by TwoFX
  1

• Meta.check does not check projections

  #5660 opened 3 months ago by nomeata
  0

• Exception.isMaxHeartbeat no longer works

  #5565 opened 3 months ago by eric-wieser
  0

• Lake fetches caches for unbuilt dependencies

  #5633 opened 3 months ago by tydeu
  0

• Duplicated error when using placeholders in `simpa`

  #5634 opened 3 months ago by TwoFX
  0

• Namespace completion inserts full name rather than remainder

  #5654 opened 3 months ago by tydeu
  0

• "(kernel) unknown constant" when specializing a mutually recursive function

  #5651 opened 3 months ago by JovanGerb
  0

• macOS clang fails to link against dylib generated by Lean

  #5649 opened 3 months ago by Kha
  0

• Cannot derive functional induction principle

  #5602 opened 3 months ago by BrunoDutertre
  2

• by? generates sorryAX instead of reporting proof

  #5625 opened 3 months ago by mars0i
  0

• Elaboration failure with let mut whose RHS is a do notation

  #5607 opened 3 months ago by bollu
  1

• Unexpected "invalid universe level" error using implicit variables

  #5621 opened 3 months ago by mdempsky
  0

• Instantiate metavars takes enormously long in VSCode, but is snappy in the terminal

  #5614 opened 3 months ago by bollu
  0

• `by decide` crash with recursive `Decidable` instances

  #5612 opened 3 months ago by TomasPuverle
  2

• exact? and apply? throw "maximum recursion depth has been reached" when large Nat constants are involved

  #5613 opened 3 months ago by bollu
  0

• Rewrite applies the wrong equational rule

  #5611 opened 3 months ago by BrunoDutertre
  3

• `simp` fails to see through `abbrev`

  #5606 opened 3 months ago by JLimperg
  0

• The build installs a copy of the already installed cadical binary

  #5603 opened 3 months ago by yurivict
  0

• RFC: `unless` doesn't support hypothesis like e.g. `if h: ...`

  #5598 opened 3 months ago by TomasPuverle
  0

• `simp!` docstring does not talk about simp!

  #5597 opened 3 months ago by nomeata
  0

• Exponential unfolding behaviour in Meta.isDefEq and Meta.whnf reduction

  #5596 opened 3 months ago by ymherklotz
  0

• "omit" doesn't omit typeclass assumptions

  #5595 opened 3 months ago by loefflerd
  0

• `simp at *` fails to close goal where `simp at h` does

  #5593 opened 3 months ago by TwoFX
  1

• Type universes and mutual definitions not working together

  #5576 opened 3 months ago by mik-jozef
  0

• bv_decide does not normalize bitvector widths

  #5575 opened 3 months ago by bollu
  1

• Header lean.h not conforming C++

  #5570 opened 3 months ago by tkoeppe
  4