exists から use へのリンクを張る

lean-ja · Dec 31, 2024 · be8e033 · be8e033
1 parent d2e5e63
commit be8e033
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/LeanByExample/Tactic/Exists.lean b/LeanByExample/Tactic/Exists.lean
@@ -8,6 +8,8 @@ import Lean --#
 example : ∃ x : Nat, 3 * x + 1 = 7 := by
   exists 2
 
+/- 上位互換にあたるタクティクに [`use`](./Use.md) タクティクがあります。 -/
+
 /- ## 舞台裏
 なお Lean での存在量化の定義は次のようになっています。-/
 --#--