-- import Mathlib
import Mathlib.Init.Data.Nat.Notation
import Mathlib.Control.Traversable.Basic
import ImportGraph.Imports

-- 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! 🐙


-- 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
#minimize_imports
import Mathlib.Control.Traversable.Basic

#find_home
[Batteries.Data.MLList.Basic,
 Batteries.Data.Nat.Gcd,
 Batteries.Data.List.Init.Attach,
 Batteries.WF,
 Batteries.Data.List.Init.Lemmas,
 Batteries.Data.Nat.Basic,
 Batteries.Data.LazyList,
 Batteries.Lean.IO.Process,
 Init.Prelude,
 Batteries.Data.Sum.Basic,
 Mathlib.Init.Data.Nat.Notation,
 Batteries.Classes.SatisfiesM,
 Batteries.Lean.Float,
 Batteries.Data.Array.Match,
 Batteries.Data.Array.Init.Lemmas,
 Batteries.Data.DList,
 Batteries.Control.ForInStep.Basic,
 Batteries.Control.Lemmas,
 Batteries.Classes.BEq,
 Batteries.Data.Fin.Basic] 
Nat: Type
Nat

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