From 52a4f535d853a2c7c7eea5fee8a4fa04c682c1ee Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 17 Apr 2021 18:48:58 +0200 Subject: [PATCH] doc: fix example --- doc/tactics.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/tactics.md b/doc/tactics.md index 6c7dfca37c..2598225316 100644 --- a/doc/tactics.md +++ b/doc/tactics.md @@ -244,7 +244,7 @@ theorem mem_split {a : α} {as : List α} (h : a ∈ as) : ∃ s t, as = s ++ a | cons b bs ih => cases h with | head a bs => exact ⟨[], ⟨bs, rfl⟩⟩ | tail a b bs h => - match bs, ih h with + match (generalizing := false) bs, ih h with | _, ⟨s, ⟨t, rfl⟩⟩ => exists b::s; exists t rw [List.cons_append]