Actions: leanprover/lean4
Actions
301 workflow runs
301 workflow runs
PANIC at outOfBounds
on theorem involving a nested inductive
Jira sync
#176:
Issue #5726
closed
by
nomeata
leanpkg
binary to help confused new users
Jira sync
#174:
Issue #2872
closed
by
Kha
show_term
and by?
change order of elaboration
Jira sync
#173:
Issue #5713
closed
by
kmill
Fin n
literals, but not n
itself
Jira sync
#168:
Issue #5630
closed
by
nomeata
bv_decide
throws an unknown free variable
error if there is an hypothesis b.toNat > 0
in the context
Jira sync
#163:
Issue #5674
closed
by
hargoniX
#eval
on let rec
causes error in kernel
Jira sync
#162:
Issue #2374
closed
by
kmill
bv_decide
regression; proof that worked before now times out, and LRAT file sizes are much larger
Jira sync
#161:
Issue #5664
closed
by
alexkeizer
simpa
type mismatch error message could be improved
Jira sync
#155:
Issue #4101
closed
by
kmill
simpa
Jira sync
#154:
Issue #5634
closed
by
kmill
structure
sometimes makes a Type
not a Prop
.
Jira sync
#153:
Issue #2690
closed
by
kmill