-- import Mathlib
-- import Batteries.Data.Nat.Basic
-- for ℕ and fixing
-- tactic 'induction' failed, major premise type is not an inductive type  
import Mathlib.Data.Nat.Notation
-- for induction
import Batteries.Tactic.Init
import Mathlib.Control.Traversable.Basic
-- for #min_imports
import ImportGraph.Imports
-- import Mathlib

-- https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Agda.20style.20interactive.20case.20splitting.3F/near/424179379
-- def foo (n : Nat) : Nat := by
--   induction n with
-- Cmd+. => Code action: generate an explicit pattern match for 'induction'
def 
foo: ℕ → ℕ
foo
Warning: declaration uses 'sorry' (
n: ℕ
n : 
ℕ: Type
ℕ) : 
ℕ: Type
ℕ := by
Goals accomplished! 🐙
  induction 
n: ℕ
n with
n: ℕ
ℕ
  | zero =>
zero
ℕ sorry
Goals accomplished! 🐙
  | succ 
n: ℕ
n 
ih: ℕ
ih =>
n, ih: ℕ
succ
ℕ sorry
Goals accomplished! 🐙

-- #help tactic induction

-- https://github.com/leanprover-community/batteries/pull/577
-- instance : Monad Id := _
-- Cmd+. => Code action: Generate a (maximal) skeleton for the structure under construction
instance: Monad Id
instance
Warning: declaration uses 'sorry' : 
Monad: (Type u_1 → Type u_1) → Type (u_1 + 1)
Monad 
Id: Type u_1 → Type u_1
Id where
  pure := 
sorry: α✝ → Id α✝
sorry
  bind := 
sorry: Id α✝ → (α✝ → Id β✝) → Id β✝
sorry

-- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60.23minimize_imports.60.20doesn't.20find.20notation.20imports
#min_imports
import Mathlib.Control.Traversable.Basic

#find_home
[Batteries.Data.List.Init.Lemmas, Mathlib.Data.Nat.Notation, Init.Prelude, Batteries.Util.ExtendedBinder] 
Nat: Type
Nat

#check
ℕ : Type 
ℕ: Type
ℕ

-- To use `shake`:
-- lake build Playground.Zulip.CodeAction
-- lake exe shake Playground.Zulip.CodeAction