We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent fa6d899 commit 42e17faCopy full SHA for 42e17fa
tests/lean/run/11455.lean
@@ -0,0 +1,3 @@
1
+-- Since `by` now has the `arg` precedence, it can be used as an argument directly:
2
+
3
+example (a : Nat) : a ≤ a := a.le_of_eq by simp
0 commit comments