From f02e591c37c4f26953e991f023f606921fb755dc Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 31 Mar 2023 17:48:04 +0200 Subject: [PATCH] typo --- server/nng/NNG/Modifications/Tactics.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/server/nng/NNG/Modifications/Tactics.lean b/server/nng/NNG/Modifications/Tactics.lean index 4a488bd..ba0aff7 100644 --- a/server/nng/NNG/Modifications/Tactics.lean +++ b/server/nng/NNG/Modifications/Tactics.lean @@ -32,7 +32,7 @@ syntax (name := rewriteSeq) "rw" (config)? rwRuleSeq (location)? : tactic # Modified `induction` tactic Modify `induction` tactic to always show `(0 : MyNat)` instead of `MyNat.zero` and -to support the lean3-style `while` keyword. +to support the lean3-style `with` keyword. This is mainly copied and modified from the mathlib-tactic `induction'`. -/