Tomáš Skřivan
Tomáš Skřivan
Ok, I will just copy it for now and let's see if it work as I hope for the needs of `fprop`. And if it does it might be a...
The next to last problem in the set file is does not work because of missing `fun_trans` feature.
I don't understand, can you give mwe?
You need to be even more clearer. `Scalar` is a class, I don't understand why should it have `Repr` instance. Do you mean that `Scalar` should extend `Repr R`? That...
This is broken for unrelated reasons now. Investigate!
This is problem again but with how `Tactic.lift_lets_simproc` works now.
I think it works as expected now when using `lsimp`
So far I have these notations where I have a custom `by` and it would be nice to have a bubble after it ``` notation term "rewrite_by" convSeq : term...
I did the exact steps as you described with `code .` and with `cd verso; emacs examples/textbook/DemoTextbook.lean ` My system: ``` $ uname -a Linux tskrivan 5.15.0-117-generic #127~20.04.1-Ubuntu SMP Thu...
I have added ``` #eval IO.getEnv "LD_LIBRARY_PATH" #eval IO.getEnv "PWD" ``` to `lakefile.lean` and `DemoTextbookMain.lean` In `lakefile.lean` the output is: interactive: ``` some "././.lake/packages/subverso/.lake/build/lib:././.lake/packages/MD4Lean/.lake/build/lib:././.lake/build/lib:/home/tskrivan/.elan/toolchains/leanprover--lean4---nightly-2024-07-12/lib/lean:/home/tskrivan/.elan/toolchains/leanprover--lean4---nightly-2024-07-12/lib" some "/home/tskrivan/Documents/verso" ``` build `lake build`:...