Commit 2021-10-21 02:55 3c11bd77View on Github →
chore(*): bump to lean 3.34.0 (#9824)
Backport coercions from Lean 4
has_coe_to_sort take the output type as an
out_param argument. This change comes with some changes in the elaboration order, so some proofs/definitions need more type annotations.
by_contra h does better job if the goal is a negation.
open and current namespace
namespace A open B _root_.C end A
Lean will try to open
A.B; if this fails, it will open
B. It will also open
setup_tactic_parser_cmd command was updated to open appropriate