Arthur Paulino
Arthur Paulino
I got farther with this: https://stackoverflow.com/questions/62612405/usr-bin-ld-cannot-find-lc Basically: `sudo apt install libc++-11-dev libc++abi-11-dev` But then: ```text [5/1332] Building CXX object third_party/tinyxml/CMakeFiles/tinyxml.dir/tinyxmlerror.cpp.o FAILED: third_party/tinyxml/CMakeFiles/tinyxml.dir/tinyxmlerror.cpp.o /usr/bin/clang++ -DCMARK_STATIC_DEFINE -DNDEBUG -DPNG_NO_MMX_CODE -DTIXML_USE_STL -I/home/arthur/apps/aseprite/aseprite/third_party/zlib -I/home/arthur/apps/aseprite/aseprite/build/third_party/zlib -I/home/arthur/apps/aseprite/aseprite/third_party/libpng...
deleting a guide causes a 500 internal server error. editing/deleting a garden changes the page temporarily but doesn't really affect the back-end since what I do is undone after I...
This PR also touches the code of the `norm_cast` tactic. Maybe it's better to split it in two different PRs? @gebner wdyt?
Gotta add it to the `Mathlib.lean` import list 👍🏼
Also, I don't understand that lint error from the CI tests
`rename_var` is not explicit enough and when looking at its name alone I was mistaken about its behavior. The fact is that this tactic only renames bound variables.
@JLimperg > I replaced your API for `modifyLocalContext` etc. with an API that is arguably more in line with the core APIs, though whether that makes it better is another...
bors r+
`and_then` is subtly different from `<;>`. The former focuses the goal, whereas the latter does not.
The problem was that `{ $a:tactic; all_goals $b:tactic }`, with curly braces, was explicitly requiring it to close the goals. Removing them solved the problem. [Commit link](https://github.com/arthurpaulino/lean4-metaprogramming-book/commit/5f5ab8bcff09c773bbfe2a1c7c12c394e5c1c4bd)
`and_then` is subtly different from `<;>`. The former focuses the goal, whereas the latter does not.
@alexkeizer the PR is highly welcome if you explain the change in the text. We're in the tactics chapter afterall 👍🏼