lean4

lean4 copied to clipboard

### Description #2462 added support for renaming, but the current implementation does not correctly deal with namespaces: ``` namespace Bar structure Foo where a : Nat def foobar (f :...

mhuisi

In the following example, `congr` fails on the term `id f a`: ``` example (a b : Nat) (f : Nat → Nat) : id f a = id f...

kmill

This papercut in error reporting has been causing me mild frustration and prevented me from figuring out syntax by trying, maybe it can be improved: ``` import Lean def bar...

nomeata

"failed to generate unfold theorem" for recursive nested match

3

### Prerequisites * [X] Put an X between the brackets on this line if you have done all of the following: * Check that your issue is not already [filed](https://github.com/leanprover/lean4/issues)....

JamesGallicchio

chore: add LNSym omega benchmarks with large problems that take multiple seconds to solve

15

bollu

chore: add example where omega never terminates / runs out of heartbeats

1

I am trying to see if removing redundant constraints from https://github.com/leanprover/lean4/pull/5657 helps `omega`. In doing so, I accidentally deleted what I think is an irredundant constraint. This problem makes omega...

bollu

### Prerequisites Please put an X between the brackets as you perform the following steps: * [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [X] Reduce the...

mdempsky

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

mars0i

``` % g++ test.cpp -o test -lleanshared -lreverseffiwithmathlib ld: __DATA_CONST segment missing SG_READ_ONLY flag in '/Users/cruis/Documents/ReverseFFIwithMathlib/.lake/build/lib/libreverseffiwithmathlib.dylib' clang: error: linker command failed with exit code 1 (use -v to see invocation)...

Kha

### Prerequisites Please put an X between the brackets as you perform the following steps: * [ ] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce...

JovanGerb