From 13ecfec8b9d7cc6969399abe9e6e7ef48c866f80 Mon Sep 17 00:00:00 2001
From: Kitamado <47292598+Seasawher@users.noreply.github.com>
Date: Fri, 22 May 2026 23:53:44 +0900
Subject: [PATCH] =?UTF-8?q?grind=5Fpattern=20=E3=81=AE=E3=83=AF=E3=82=A4?=
 =?UTF-8?q?=E3=83=AB=E3=83=89=E3=82=AB=E3=83=BC=E3=83=89=E4=BE=8B=E3=82=92?=
 =?UTF-8?q?=E8=BF=BD=E5=8A=A0?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Declarative/GrindPattern.lean | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/LeanByExample/Declarative/GrindPattern.lean b/LeanByExample/Declarative/GrindPattern.lean
index 1daff63f..c8933964 100644
--- a/LeanByExample/Declarative/GrindPattern.lean
+++ b/LeanByExample/Declarative/GrindPattern.lean
@@ -17,6 +17,25 @@ example (x y z : Nat) (h₁ : R x y) (h₂ : R y z) : R x z := by
   -- grind で証明できる
   grind
 
+/- パターンの中では、通常の項と同じように `_` でワイルドカードを指定できます。
+ただし、定理をインスタンス化するために必要なパラメータは、どこかのパターンでカバーされていなければなりません。
+次の例では、`S x y` が `x` と `y` をカバーし、`S _ z` が `z` をカバーしています。-/
+
+namespace WildcardPattern --#
+
+/-- 何らかの二項関係 -/
+opaque S : Nat → Nat → Prop
+
+/-- S は推移的 -/
+axiom Strans {x y z : Nat} : S x y → S y z → S x z
+
+grind_pattern Strans => S x y, S _ z
+
+example (x y z : Nat) (h₁ : S x y) (h₂ : S y z) : S x z := by
+  grind
+
+end WildcardPattern --#
+
 /-
 ## `[grind]` 属性では登録できない例