Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

「index in target's type is not a variable」エラーはいつ起こるのか？ #1064

Merged
merged 1 commit into from
Nov 6, 2024
Merged

「index in target's type is not a variable」エラーはいつ起こるのか？ #1064

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 29 additions & 0 deletions LeanByExample/Reference/Tactic/Induction.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -186,6 +186,35 @@ def bar : Nat → Nat
#guard_msgs (drop warning) in --#
#check_failure bar.induct

/- ## よくあるエラー
`induction` タクティクを使ったときに、`index in target's type is not a variable` というエラーが出ることがあります。
-/

/-- 偶数であることを表す帰納的述語 -/
inductive MyEven : Nat → Prop where
| zero : MyEven 0
| succ : {n : Nat} → MyEven n → MyEven (n + 2)

/--
error: index in target's type is not a variable (consider using the `cases` tactic instead)
0
-/
#guard_msgs in
example (h : MyEven 0) : True := by
induction h

/- これは型族の添え字が変数ではないから起こることです。その証拠に、変数にするとエラーにならなくなります。-/

example (n m : Nat) (h : MyEven (n + m)) : True := by
/-
index in target's type is not a variable (consider using the `cases` tactic instead)
n + m
-/
generalize n + m = x at h
induction h
· trivial
· trivial

/-
[^recursive]: [lean公式ブログの Functional induction についての記事](https://lean-lang.org/blog/2024-5-17-functional-induction/) で recursive theorem という言葉が使われています。
-/