feat: subst notation (heq ▸ h) tries both orientation

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

3.82k stars 325 forks source link

Closed nomeata closed 2 weeks ago

nomeata commented 2 weeks ago

even when rewriting the type of h becuase there is no expected type.

(When there is an expected type, it already tried both orientations.)

Also feeble attempt to include this information in the docstring without writing half a manual chapter.

leanprover-community-mathlib4-bot commented 2 weeks ago

Mathlib CI status (docs):

❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d9ea0925853818660ff4869ef11bcacfaec9b7d7 --onto 83c139f7504706624eb3dcb3d78000d4fc6f4d13. (2024-05-01 19:56:05)