Commit 2021-10-21 02:55 3c11bd77

chore(*): bump to lean 3.34.0 (#9824)

Backport coercions from Lean 4

Now has_coe_to_fun and 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.

Smarter by_contra

Now by_contra h does better job if the goal is a negation.

open and current namespace

In

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 C. setup_tactic_parser_cmd command was updated to open appropriate _root_.* namespaces.