/-
Copyright (c) 2022 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
import Mathlib.Lean.Expr.Basic

/-!

# The `#help` command

The `#help` command can be used to list all definitions in a variety of extensible aspects of lean.

* `#help option` lists options (used in `set_option myOption`)
* `#help attr` lists attributes (used in `@[myAttr] def foo := ...`)
* `#help cats` lists syntax categories (like `term`, `tactic`, `stx` etc)
* `#help cat C` lists elements of syntax category C
  * `#help term`, `#help tactic`, `#help conv`, `#help command`
    are shorthand for `#help cat term` etc.
  * `#help cat+ C` also shows `elab` and `macro` definitions associated to the syntaxes

All forms take an optional identifier to narrow the search; for example `#help option pp` shows
only `pp.*` options.

-/

namespace Mathlib.Tactic
open Lean Meta Elab Tactic Command

/--
The command `#help option` shows all options that have been defined in the current environment.
Each option has a format like:
```
option pp.all : Bool := false
  (pretty printer) display coercions, implicit parameters, proof terms, fully qualified names,
  universe, and disable beta reduction and notations during pretty printing
```
This says that `pp.all` is an option which can be set to a `Bool` value, and the default value is
`false`. If an option has been modified from the default using e.g. `set_option pp.all true`,
it will appear as a `(currently: true)` note next to the option.

The form `#help option id` will show only options that begin with `id`.
-/
elab "#help" &: String → Bool → ParserDescr
&"option" id: ?m.94
id:(ident: Parser.Parser
ident)? : command: Parser.Category
command => do
  let id: ?m.159
id := id: ?m.94
id.map: {α : Type ?u.161} → {β : Type ?u.160} → (α → β) → Option α → Option β
map (·.getId: Ident → Name
getId.toString: Name → optParam Bool true → String
toString false: Bool
false)
  let mut decls: RBMap ?m.178 ?m.179 compare
decls : Lean.RBMap: (α : Type ?u.177) → Type ?u.176 → (α → α → Ordering) → Type (max?u.177?u.176)
Lean.RBMap _: Type ?u.177
_ _: Type ?u.176
_ compare: {α : Type ?u.180} → [self : Ord α] → α → α → Ordering
compare := {}: ?m.193
{}
  for (name: Name
name, decl: OptionDecl
decl) in show Lean.RBMap: (α : Type ?u.349) → Type ?u.348 → (α → α → Ordering) → Type (max?u.349?u.348)
Lean.RBMap .. from ← getOptionDecls: IO OptionDecls
getOptionDecls do
    let name: ?m.476
name := name: Name
name.toString: Name → optParam Bool true → String
toString false: Bool
false
    if let some: {α : Type ?u.140} → α → Option α
some id: String
id := id: ?m.159
id then
      if !id: String
id.isPrefixOf: String → String → Bool
isPrefixOf name: ?m.476
name then
        continue
    decls: ?m.473
decls := decls: RBMap ?m.181 ?m.179 compare
decls.insert: {α : Type ?u.922} → {β : Type ?u.921} → {cmp : α → α → Ordering} → RBMap α β cmp → α → β → RBMap α β cmp
insert name: ?m.476
name decl: OptionDecl
decl
  let mut msg: Format
msg := Format.nil: Format
Format.nil
  let opts: ?m.1554
opts ← getOptions: {m : Type → Type} → [self : MonadOptions m] → m Options
getOptions
  if decls: ?m.1498
decls.isEmpty: {α : Type ?u.1570} → {β : Type ?u.1569} → {cmp : α → α → Ordering} → RBMap α β cmp → Bool
isEmpty then
    match id: ?m.159
id with
    | some: {α : Type ?u.143} → α → Option α
some id: String
id => throwError "no options start with {id: String
id}"
    | none: {α : Type ?u.147} → Option α
none => throwError "no options found (!)": ?m.1980 ?m.1981
throwErrorthrowError "no options found (!)": ?m.1980 ?m.1981
 "no options found (!)"
  for (name: String
name, decl: OptionDecl
decl) in decls: ?m.1498
decls do
    let mut msg1: ?m.2387
msg1 := match decl: OptionDecl
decl.defValue: OptionDecl → DataValue
defValue with
    | .ofString: String → DataValue
.ofString val: String
val => s!"String := {repr: {α : Type ?u.2880} → [inst : Repr α] → α → Format
repr val: String
val}"
    | .ofBool: Bool → DataValue
.ofBool val: Bool
val => s!"Bool := {repr: {α : Type ?u.2976} → [inst : Repr α] → α → Format
repr val: Bool
val}"
    | .ofName: Name → DataValue
.ofName val: Name
val => s!"Name := {repr: {α : Type ?u.3070} → [inst : Repr α] → α → Format
repr val: Name
val}"
    | .ofNat: Nat → DataValue
.ofNat val: Nat
val => s!"Nat := {repr: {α : Type ?u.3164} → [inst : Repr α] → α → Format
repr val: Nat
val}"
    | .ofInt: Int → DataValue
.ofInt val: Int
val => s!"Int := {repr: {α : Type ?u.3258} → [inst : Repr α] → α → Format
repr val: Int
val}"
    | .ofSyntax: Syntax → DataValue
.ofSyntax val: Syntax
val => s!"Syntax := {repr: {α : Type ?u.3352} → [inst : Repr α] → α → Format
repr val: Syntax
val}"
    if let some: {α : Type ?u.2488} → α → Option α
some val: DataValue
val := opts: ?m.1554
opts.find: KVMap → Name → Option DataValue
find name: String
name then
      msg1: ?m.2504
msg1 := s!"{msg1: ?m.2387
msg1}  (currently: {val: DataValue
val})"
    msg: Format
msg := msg: Format
msg ++ .nest: Int → Format → Format
.nest 2: ?m.3916
2 (f!"option {name: String
name} : {msg1: ?m.2387
msg1}" ++ .line: Format
.line ++ decl: OptionDecl
decl.descr: OptionDecl → String
descr) ++ .line: Format
.line ++ .line: Format
.line
  logInfo: {m : Type → Type} →
  [inst : Monad m] → [inst : MonadLog m] → [inst : AddMessageContext m] → [inst : MonadOptions m] → MessageData → m Unit
logInfo msg: ?m.4284
msg

/--
The command `#help attribute` (or the short form `#help attr`) shows all attributes that have been
defined in the current environment.
Each option has a format like:
```
[inline]: mark definition to always be inlined
```
This says that `inline` is an attribute that can be placed on definitions like
`@[inline] def foo := 1`. (Individual attributes may have restrictions on where they can be
applied; see the attribute's documentation for details.) Both the attribute's `descr` field as well
as the docstring will be displayed here.

The form `#help attr id` will show only attributes that begin with `id`.
-/
elab "#help" (&: String → Bool → ParserDescr
&"attr" <|> &: String → Bool → ParserDescr
&"attribute") id: ?m.12012
id:(ident: Parser.Parser
ident)? : command: Parser.Category
command => do
  let id: ?m.12081
id := id: ?m.12012
id.map: {α : Type ?u.12083} → {β : Type ?u.12082} → (α → β) → Option α → Option β
map (·.getId: Ident → Name
getId.toString: Name → optParam Bool true → String
toString false: Bool
false)
  let mut decls: ?m.12514
decls : Lean.RBMap: (α : Type ?u.12099) → Type ?u.12098 → (α → α → Ordering) → Type (max?u.12099?u.12098)
Lean.RBMap _: Type ?u.12099
_ _: Type ?u.12098
_ compare: {α : Type ?u.12102} → [self : Ord α] → α → α → Ordering
compare := {}: ?m.12115
{}
  for (name: Name
name, decl: AttributeImpl
decl) in ← attributeMapRef: IO.Ref (PersistentHashMap Name AttributeImpl)
attributeMapRef.get: {σ : Type} → {m : Type → Type} → [inst : MonadLiftT (ST σ) m] → {α : Type} → ST.Ref σ α → m α
get do
    let name: ?m.12517
name := name: Name
name.toString: Name → optParam Bool true → String
toString false: Bool
false
    if let some: {α : Type ?u.13109} → α → Option α
some id: String
id := id: ?m.12081
id then
      if !id: String
id.isPrefixOf: String → String → Bool
isPrefixOf name: ?m.12517
name then
        continue
    decls: RBMap ?m.12103 ?m.12101 compare
decls := decls: RBMap ?m.12103 ?m.12101 compare
decls.insert: {α : Type ?u.12955} → {β : Type ?u.12954} → {cmp : α → α → Ordering} → RBMap α β cmp → α → β → RBMap α β cmp
insert name: ?m.12517
name decl: AttributeImpl
decl
  let mut msg: Format
msg := Format.nil: Format
Format.nil
  let env: ?m.13574
env ← getEnv: {m : Type → Type} → [self : MonadEnv m] → m Environment
getEnv
  if decls: ?m.13518
decls.isEmpty: {α : Type ?u.13590} → {β : Type ?u.13589} → {cmp : α → α → Ordering} → RBMap α β cmp → Bool
isEmpty then
    match id: ?m.12081
id with
    | some: {α : Type ?u.12065} → α → Option α
some id: String
id => throwError "no attributes start with {id: String
id}"
    | none: {α : Type ?u.12069} → Option α
none => throwError "no attributes found (!)": ?m.14000 ?m.14001
throwErrorthrowError "no attributes found (!)": ?m.14000 ?m.14001
 "no attributes found (!)"
  for (name: String
name, decl: AttributeImpl
decl) in decls: ?m.13518
decls do
    let mut msg1: ?m.14367
msg1 := s!"[{name: String
name}]: {decl: AttributeImpl
decl.descr: AttributeImplCore → String
descr}"
    if let some: {α : Type ?u.14555} → α → Option α
some doc: String
doc ← findDocString?: Environment → Name → optParam Bool true → IO (Option String)
findDocString? env: ?m.13574
env decl: AttributeImpl
decl.ref: AttributeImplCore → Name
ref then
      msg1: ?m.14367
msg1 := s!"{msg1: ?m.14367
msg1}\n{doc: String
doc.trim: String → String
trim}"
    msg: ?m.14364
msg := msg: Format
msg ++ .nest: Int → Format → Format
.nest 2: ?m.15137
2 msg1: String
msg1 ++ .line: Format
.line ++ .line: Format
.line
  logInfo: {m : Type → Type} →
  [inst : Monad m] → [inst : MonadLog m] → [inst : AddMessageContext m] → [inst : MonadOptions m] → MessageData → m Unit
logInfo msg: ?m.15277
msg

/-- Gets the initial string token in a parser description. For example, for a declaration like
`syntax "bla" "baz" term : tactic`, it returns `some "bla"`. Returns `none` for syntax declarations
that don't start with a string constant. -/
partial def getHeadTk: Expr → Option String
getHeadTk (e: Expr
e : Expr: Type
Expr) : Option: Type ?u.22223 → Type ?u.22223
Option String: Type
String :=
  match e: Expr
e.getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs with
  | (``ParserDescr.node: Name
``ParserDescr.node: SyntaxNodeKind → Nat → ParserDescr → ParserDescr
ParserDescr.node, #[_, _, p: Expr
p]) => getHeadTk: Expr → Option String
getHeadTk p: Expr
p
  | (``ParserDescr.unary: Name
``ParserDescr.unary: Name → ParserDescr → ParserDescr
ParserDescr.unary, #[.app: Expr → Expr → Expr
.app _ (.lit: Literal → Expr
.lit (.strVal: String → Literal
.strVal "withPosition": String
"withPosition")), p: Expr
p]) => getHeadTk: Expr → Option String
getHeadTk p: Expr
p
  | (``ParserDescr.unary: Name
``ParserDescr.unary: Name → ParserDescr → ParserDescr
ParserDescr.unary, #[.app: Expr → Expr → Expr
.app _ (.lit: Literal → Expr
.lit (.strVal: String → Literal
.strVal "atomic": String
"atomic")), p: Expr
p]) => getHeadTk: Expr → Option String
getHeadTk p: Expr
p
  | (``ParserDescr.binary: Name
``ParserDescr.binary: Name → ParserDescr → ParserDescr → ParserDescr
ParserDescr.binary, #[.app: Expr → Expr → Expr
.app _ (.lit: Literal → Expr
.lit (.strVal: String → Literal
.strVal "andthen": String
"andthen")), p: Expr
p, _]) => getHeadTk: Expr → Option String
getHeadTk p: Expr
p
  | (``ParserDescr.nonReservedSymbol: Name
``ParserDescr.nonReservedSymbol: String → Bool → ParserDescr
ParserDescr.nonReservedSymbol, #[.lit: Literal → Expr
.lit (.strVal: String → Literal
.strVal tk: String
tk), _]) => some: {α : Type ?u.22482} → α → Option α
some tk: String
tk
  | (``ParserDescr.symbol: Name
``ParserDescr.symbol: String → ParserDescr
ParserDescr.symbol, #[.lit: Literal → Expr
.lit (.strVal: String → Literal
.strVal tk: String
tk)]) => some: {α : Type ?u.22520} → α → Option α
some tk: String
tk
  | (``Parser.withAntiquot: Name
``Parser.withAntiquot: Parser.Parser → Parser.Parser → Parser.Parser
Parser.withAntiquot, #[_, p: Expr
p]) => getHeadTk: Expr → Option String
getHeadTk p: Expr
p
  | (``Parser.leadingNode: Name
``Parser.leadingNode: SyntaxNodeKind → Nat → Parser.Parser → Parser.Parser
Parser.leadingNode, #[_, _, p: Expr
p]) => getHeadTk: Expr → Option String
getHeadTk p: Expr
p
  | (``HAndThen.hAndThen: Name
``HAndThen.hAndThen: {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HAndThen α β γ] → α → (Unit → β) → γ
HAndThen.hAndThen, #[_, _, _, _, p: Expr
p, _]) => getHeadTk: Expr → Option String
getHeadTk p: Expr
p
  | (``Parser.nonReservedSymbol: Name
``Parser.nonReservedSymbol: String → optParam Bool false → Parser.Parser
Parser.nonReservedSymbol, #[.lit: Literal → Expr
.lit (.strVal: String → Literal
.strVal tk: String
tk), _]) => some: {α : Type ?u.22761} → α → Option α
some tk: String
tk
  | (``Parser.symbol: Name
``Parser.symbol: String → Parser.Parser
Parser.symbol, #[.lit: Literal → Expr
.lit (.strVal: String → Literal
.strVal tk: String
tk)]) => some: {α : Type ?u.22798} → α → Option α
some tk: String
tk
  | _ => none: {α : Type ?u.22807} → Option α
none

/--
The command `#help cats` shows all syntax categories that have been defined in the
current environment.
Each syntax has a format like:
```
category command [Lean.Parser.initFn✝]
```
The name of the syntax category in this case is `command`, and `Lean.Parser.initFn✝` is the
name of the declaration that introduced it. (It is often an anonymous declaration like this,
but you can click to go to the definition.) It also shows the doc string if available.

The form `#help cats id` will show only syntax categories that begin with `id`.
-/
elab "#help" &: String → Bool → ParserDescr
&"cats" id: ?m.34909
id:(ident: Parser.Parser
ident)? : command: Parser.Category
command => do
  let id: ?m.34974
id := id: ?m.34909
id.map: {α : Type ?u.34976} → {β : Type ?u.34975} → (α → β) → Option α → Option β
map (·.getId: Ident → Name
getId.toString: Name → optParam Bool true → String
toString false: Bool
false)
  let mut decls: RBMap ?m.34993 ?m.34994 compare
decls : Lean.RBMap: (α : Type ?u.34992) → Type ?u.34991 → (α → α → Ordering) → Type (max?u.34992?u.34991)
Lean.RBMap _: Type ?u.34992
_ _: Type ?u.34991
_ compare: {α : Type ?u.34995} → [self : Ord α] → α → α → Ordering
compare := {}: ?m.35008
{}
  for (name: Name
name, cat: Parser.ParserCategory
cat) in (Parser.parserExtension: Parser.ParserExtension
Parser.parserExtension.getState: {σ α β : Type} → [inst : Inhabited σ] → ScopedEnvExtension α β σ → Environment → σ
getState (← getEnv): ?m.35107
(← getEnv: {m : Type → Type} → [self : MonadEnv m] → m Environment
getEnv(← getEnv): ?m.35107
)).categories: Parser.ParserExtension.State → Parser.ParserCategories
categories do
    let name: ?m.35267
name := name: Name
name.toString: Name → optParam Bool true → String
toString false: Bool
false
    if let some: {α : Type ?u.34955} → α → Option α
some id: String
id := id: ?m.34974
id then
      if !id: String
id.isPrefixOf: String → String → Bool
isPrefixOf name: ?m.35267
name then
        continue
    decls: RBMap ?m.34996 ?m.34994 compare
decls := decls: RBMap ?m.34996 ?m.34994 compare
decls.insert: {α : Type ?u.35713} → {β : Type ?u.35712} → {cmp : α → α → Ordering} → RBMap α β cmp → α → β → RBMap α β cmp
insert name: ?m.35267
name cat: Parser.ParserCategory
cat
  let mut msg: MessageData
msg := MessageData.nil: MessageData
MessageData.nil
  let env: ?m.36333
env ← getEnv: {m : Type → Type} → [self : MonadEnv m] → m Environment
getEnv
  if decls: ?m.36277
decls.isEmpty: {α : Type ?u.36349} → {β : Type ?u.36348} → {cmp : α → α → Ordering} → RBMap α β cmp → Bool
isEmpty then
    match id: ?m.34974
id with
    | some: {α : Type ?u.36449} → α → Option α
some id: String
id => throwError "no syntax categories start with {id: String
id}"
    | none: {α : Type ?u.36715} → Option α
none => throwError "no syntax categories found (!)": ?m.36759 ?m.36760
throwErrorthrowError "no syntax categories found (!)": ?m.36759 ?m.36760
 "no syntax categories found (!)"
  for (name: String
name, cat: Parser.ParserCategory
cat) in decls: ?m.36277
decls do
    let mut msg1: ?m.37126
msg1 := m!"category {name: String
name} [{mkConst: Name → optParam (List Level) [] → Expr
mkConst cat: Parser.ParserCategory
cat.declName: Parser.ParserCategory → Name
declName}]"
    if let some: {α : Type ?u.34970} → α → Option α
some doc: String
doc ← findDocString?: Environment → Name → optParam Bool true → IO (Option String)
findDocString? env: ?m.36333
env cat: Parser.ParserCategory
cat.declName: Parser.ParserCategory → Name
declName then
      msg1: ?m.37318
msg1 := msg1: ?m.37126
msg1 ++ Format.line: Format
Format.line ++ doc: String
doc.trim: String → String
trim
    msg: ?m.37123
msg := msg: MessageData
msg ++ .nest: Nat → MessageData → MessageData
.nest 2: ?m.38157
2 msg1: MessageData
msg1 ++ (.line: Format
.line ++ .line: Format
.line : Format: Type
Format)
  logInfo: {m : Type → Type} →
  [inst : Monad m] → [inst : MonadLog m] → [inst : AddMessageContext m] → [inst : MonadOptions m] → MessageData → m Unit
logInfo msg: ?m.38239
msg

/--
The command `#help cat C` shows all syntaxes that have been defined in syntax category `C` in the
current environment.
Each syntax has a format like:
```
syntax "first"... [Parser.tactic.first]
  `first | tac | ...` runs each `tac` until one succeeds, or else fails.
```
The quoted string is the leading token of the syntax, if applicable. It is followed by the full
name of the syntax (which you can also click to go to the definition), and the documentation.

* The form `#help cat C id` will show only attributes that begin with `id`.
* The form `#help cat+ C` will also show information about any `macro`s and `elab`s
  associated to the listed syntaxes.
-/
elab "#help" &: String → Bool → ParserDescr
&"cat" more: ?m.44993
more:"+"? catStx: ?m.44986
catStx:ident: Parser.Parser
ident id: ?m.44970
id:(ident: Parser.Parser
ident <|> str: Parser.Parser
str)? : command: Parser.Category
command => do
  let id: ?m.45069
id := id: ?m.44970
id.map: {α : Type ?u.45071} → {β : Type ?u.45070} → (α → β) → Option α → Option β
map fun id: ?m.45079
id ↦ match id: ?m.45079
id.raw: {ks : SyntaxNodeKinds} → TSyntax ks → Syntax
raw with
    | .ident: SourceInfo → Substring → Name → List Syntax.Preresolved → Syntax
.ident _ _ v: Name
v _ => v: Name
v.toString: Name → optParam Bool true → String
toString false: Bool
false
    | id: Syntax
id => id: Syntax
id.isStrLit?: Syntax → Option String
isStrLit?.get!: {α : Type ?u.96635} → [inst : Inhabited α] → Option α → α
get!
  let mut decls: RBMap ?m.45088 ?m.45089 compare
decls : Lean.RBMap: (α : Type ?u.45087) → Type ?u.45086 → (α → α → Ordering) → Type (max?u.45087?u.45086)
Lean.RBMap _: Type ?u.45087
_ _: Type ?u.45086
_ compare: {α : Type ?u.45090} → [self : Ord α] → α → α → Ordering
compare := {}: ?m.45103
{}
  let mut rest: RBMap ?m.45159 ?m.45160 compare
rest : Lean.RBMap: (α : Type ?u.45158) → Type ?u.45157 → (α → α → Ordering) → Type (max?u.45158?u.45157)
Lean.RBMap _: Type ?u.45158
_ _: Type ?u.45157
_ compare: {α : Type ?u.45161} → [self : Ord α] → α → α → Ordering
compare := {}: ?m.45174
{}
  let catName: ?m.45228
catName := catStx: ?m.44986
catStx.getId: Ident → Name
getId.eraseMacroScopes: Name → Name
eraseMacroScopes
  let some: {α : Type ?u.45030} → α → Option α
some cat: Parser.ParserCategory
cat := (Parser.parserExtension: Parser.ParserExtension
Parser.parserExtension.getState: {σ α β : Type} → [inst : Inhabited σ] → ScopedEnvExtension α β σ → Environment → σ
getState (← getEnv): ?m.45280
(← getEnv: {m : Type → Type} → [self : MonadEnv m] → m Environment
getEnv(← getEnv): ?m.45280
)).categories: Parser.ParserExtension.State → Parser.ParserCategories
categories.find?: {α : Type ?u.45302} → {β : Type ?u.45301} → {x : BEq α} → {x_1 : Hashable α} → PersistentHashMap α β → α → Option β
find? catName: ?m.45228
catName
    | throwErrorAt catStx: ?m.44986
catStx "{catStx: ?m.44986
catStx} is not a syntax category"
  liftTermElabM: {α : Type} → TermElabM α → CommandElabM α
liftTermElabM <| Term.addCategoryInfo: Syntax → Name → TermElabM Unit
Term.addCategoryInfo catStx: ?m.44986
catStx catName: ?m.45228
catName
  let env: ?m.45542
env ← getEnv: {m : Type → Type} → [self : MonadEnv m] → m Environment
getEnv
  for (k: SyntaxNodeKind
k, _) in cat: Parser.ParserCategory
cat.kinds: Parser.ParserCategory → Parser.SyntaxNodeKindSet
kinds do
    let mut used: ?m.45699
used := false: Bool
false
    if let some: {α : Type ?u.45039} → α → Option α
some tk: String
tk := do getHeadTk: Expr → Option String
getHeadTk (← (← env.find? k).value?): ?m.96860
(← (← env.find? k): ?m.96820
(← env: ?m.45542
env(← env.find? k): ?m.96820
.find?: Environment → Name → Option ConstantInfo
find?(← env.find? k): ?m.96820
 k: SyntaxNodeKind
k(← env.find? k): ?m.96820
)(← (← env.find? k).value?): ?m.96860
.value?: ConstantInfo → Option Expr
value?(← (← env.find? k).value?): ?m.96860
) then
      let tk: ?m.96897
tk := tk: String
tk.trim: String → String
trim
      if let some: {α : Type ?u.96916} → α → Option α
some id: String
id := id: ?m.45069
id then
        if !id: String
id.isPrefixOf: String → String → Bool
isPrefixOf tk: ?m.96897
tk then
          continue
      used: Bool
used := true: Bool
true
      decls: RBMap ?m.45091 ?m.45089 compare
decls := decls: RBMap (?m.84738 __discr✝⁶ __discr✝⁵ __discr✝⁴ __discr✝³ __discr✝² __discr✝¹ id✝ catStx more x✝³ x✝²)
  (?m.84740 __discr✝⁶ __discr✝⁵ __discr✝⁴ __discr✝³ __discr✝² __discr✝¹ id✝ catStx more x✝³ x✝²) compare
decls.insert: {α : Type ?u.97372} → {β : Type ?u.97371} → {cmp : α → α → Ordering} → RBMap α β cmp → α → β → RBMap α β cmp
insert tk: ?m.96897
tk ((decls: RBMap (?m.84738 __discr✝⁶ __discr✝⁵ __discr✝⁴ __discr✝³ __discr✝² __discr✝¹ id✝ catStx more x✝³ x✝²)
  (?m.84740 __discr✝⁶ __discr✝⁵ __discr✝⁴ __discr✝³ __discr✝² __discr✝¹ id✝ catStx more x✝³ x✝²) compare
decls.findD: {α : Type ?u.97412} → {β : Type ?u.97411} → {cmp : α → α → Ordering} → RBMap α β cmp → α → β → β
findD tk: ?m.96897
tk #[]: Array ?m.97425
#[]).push: {α : Type ?u.97454} → Array α → α → Array α
push k: SyntaxNodeKind
k)
    if !used: Bool
used && id: ?m.45069
id.isNone: {α : Type ?u.45730} → Option α → Bool
isNone then
      rest: ?m.45693
rest := rest: RBMap ?m.45162 ?m.45160 compare
rest.insert: {α : Type ?u.45810} → {β : Type ?u.45809} → {cmp : α → α → Ordering} → RBMap α β cmp → α → β → RBMap α β cmp
insert (k: SyntaxNodeKind
k.toString: Name → optParam Bool true → String
toString false: Bool
false) k: SyntaxNodeKind
k
  let mut msg: ?m.103428
msg := MessageData.nil: MessageData
MessageData.nil
  if decls: RBMap String (Array SyntaxNodeKind) compare
decls.isEmpty: {α : Type ?u.99681} → {β : Type ?u.99680} → {cmp : α → α → Ordering} → RBMap α β cmp → Bool
isEmpty && rest: RBMap String SyntaxNodeKind compare
rest.isEmpty: {α : Type ?u.99692} → {β : Type ?u.99691} → {cmp : α → α → Ordering} → RBMap α β cmp → Bool
isEmpty then
    match id: ?m.45069
id with
    | some: {α : Type ?u.99765} → α → Option α
some id: String
id => throwError "no {catName: ?m.45228
catName} declarations start with {id: String
id}"
    | none: {α : Type ?u.45054} → Option α
none => throwError "no {catName: ?m.45228
catName} declarations found"
  let env: ?m.100315
env ← getEnv: {m : Type → Type} → [self : MonadEnv m] → m Environment
getEnv
  let addMsg: SyntaxNodeKind → MessageData → MessageData → CommandElabM MessageData
addMsg (k: SyntaxNodeKind
k : SyntaxNodeKind: Type
SyntaxNodeKind) (msg: MessageData
msg msg1: MessageData
msg1 : MessageData: Type
MessageData) : CommandElabM: Type → Type
CommandElabM MessageData: Type
MessageData := do
    let mut msg1: ?m.100333
msg1 := msg1: MessageData
msg1
    if let some: {α : Type ?u.100329} → α → Option α
some doc: String
doc ← findDocString?: Environment → Name → optParam Bool true → IO (Option String)
findDocString? env: ?m.100315
env k: SyntaxNodeKind
k then
      msg1: ?m.100333
msg1 := msg1: ?m.100333
msg1 ++ Format.line: Format
Format.line ++ doc: String
doc.trim: String → String
trim
    msg1: ?m.100851
msg1 := .nest: Nat → MessageData → MessageData
.nest 2: ?m.100853
2 msg1: MessageData
msg1
    if more: ?m.44993
more.isSome: {α : Type ?u.100869} → Option α → Bool
isSome then
      let addElabs: {α : Type} → String → KeyedDeclsAttribute α → MessageData → CommandElabM MessageData
addElabs {α: ?m.100878
α} (type: String
type : String: Type
String) (attr: KeyedDeclsAttribute α
attr : KeyedDeclsAttribute: Type → Type
KeyedDeclsAttribute α: ?m.100878
α)
          (msg: MessageData
msg : MessageData: Type
MessageData) : CommandElabM: Type → Type
CommandElabM MessageData: Type
MessageData := do
        let mut msg: ?m.100988
msg := msg: MessageData
msg
        for e: ?m.100982
e in attr: KeyedDeclsAttribute α
attr.getEntries: {γ : Type} → KeyedDeclsAttribute γ → Environment → Name → List (KeyedDeclsAttribute.AttributeEntry γ)
getEntries env: ?m.100315
env k: SyntaxNodeKind
k do
          let x: ?m.100991
x := e: ?m.100982
e.declName: KeyedDeclsAttribute.OLeanEntry → Name
declName
          msg: ?m.100995
msg := msg: ?m.100988
msg ++ Format.line: Format
Format.line ++ m!"+ {type: String
type} {mkConst: Name → optParam (List Level) [] → Expr
mkConst x: ?m.100991
x}"
          if let some: {α : Type ?u.100892} → α → Option α
some doc: String
doc ← findDocString?: Environment → Name → optParam Bool true → IO (Option String)
findDocString? env: ?m.100315
env x: ?m.100991
x then
            msg: ?m.101254
msg := msg: ?m.100995
msg ++ .nest: Nat → MessageData → MessageData
.nest 2: ?m.101492
2 (Format.line: Format
Format.line ++ doc: String
doc.trim: String → String
trim)
        pure: {f : Type ?u.101767 → Type ?u.101766} → [self : Pure f] → {α : Type ?u.101767} → α → f α
pure msg: ?m.101764
msg
      msg1: ?m.100851
msg1 ← addElabs: {α : Type} → String → KeyedDeclsAttribute α → MessageData → CommandElabM MessageData
addElabs "macro": String
"macro" macroAttribute: KeyedDeclsAttribute Macro
macroAttribute msg1: ?m.100851
msg1
      match catName: ?m.45228
catName with
      | `term: Name
`term => msg1: ?m.101854
msg1 ← addElabs: {α : Type} → String → KeyedDeclsAttribute α → MessageData → CommandElabM MessageData
addElabs "term elab": String
"term elab" Term.termElabAttribute: KeyedDeclsAttribute Term.TermElab
Term.termElabAttribute msg1: ?m.101854
msg1
      | `command: Name
`command => msg1: ?m.101854
msg1 ← addElabs: {α : Type} → String → KeyedDeclsAttribute α → MessageData → CommandElabM MessageData
addElabs "command elab": String
"command elab" commandElabAttribute: KeyedDeclsAttribute CommandElab
commandElabAttribute msg1: ?m.101854
msg1
      | `tactic: Name
`tactic | `conv: Name
`conv => msg1: ?m.101854
msg1 ← addElabs: {α : Type} → String → KeyedDeclsAttribute α → MessageData → CommandElabM MessageData
addElabs "tactic elab": String
"tactic elab" tacticElabAttribute: KeyedDeclsAttribute Tactic
tacticElabAttribute msg1: ?m.101854
msg1
      | _ => pure: {f : Type ?u.102459 → Type ?u.102458} → [self : Pure f] → {α : Type ?u.102459} → α → f α
pure (): Unit
()
    return msg: MessageData
msg ++ msg1: MessageData
msg1 ++ (.line: Format
.line ++ .line: Format
.line : Format: Type
Format)
  for (name: String
name, ks: Array SyntaxNodeKind
ks) in decls: RBMap String (Array SyntaxNodeKind) compare
decls do
    for k: ?m.103506
k in ks: Array SyntaxNodeKind
ks do
      msg: ?m.103693
msg ← addMsg: SyntaxNodeKind → MessageData → MessageData → CommandElabM MessageData
addMsg k: ?m.103506
k msg: ?m.103512
msg m!"syntax {repr: {α : Type ?u.103572} → [inst : Repr α] → α → Format
repr name: String
name}... [{mkConst: Name → optParam (List Level) [] → Expr
mkConst k: ?m.103506
k}]"
  for (_, k: SyntaxNodeKind
k) in rest: RBMap String SyntaxNodeKind compare
rest do
    msg: ?m.104277
msg ← addMsg: SyntaxNodeKind → MessageData → MessageData → CommandElabM MessageData
addMsg k: SyntaxNodeKind
k msg: ?m.104163
msg m!"syntax ... [{mkConst: Name → optParam (List Level) [] → Expr
mkConst k: SyntaxNodeKind
k}]"
  logInfo: {m : Type → Type} →
  [inst : Monad m] → [inst : MonadLog m] → [inst : AddMessageContext m] → [inst : MonadOptions m] → MessageData → m Unit
logInfo msg: ?m.104513
msg

/--
The command `#help term` shows all term syntaxes that have been defined in the current environment.
See `#help cat` for more information.
-/
macro "#help" tk: ?m.128819
tk:&: String → Bool → ParserDescr
&"term" more: ?m.128806
more:"+"? id: ?m.128790
id:(ident: Parser.Parser
ident <|> str: Parser.Parser
str)? : command: Parser.Category
command =>
  `(#help cat$[+%$more: TSyntax Name.anonymous
more]? $(mkIdentFrom: Syntax → Name → optParam Bool false → Ident
mkIdentFrom tk: ?m.128819
tk `term: Name
`term) $(id: ?m.128790
id.map: {α : Type ?u.129329} → {β : Type ?u.129328} → (α → β) → Option α → Option β
map (⟨·.raw: {ks : SyntaxNodeKinds} → TSyntax ks → Syntax
raw⟩))?)

/--
The command `#help tactic` shows all tactics that have been defined in the current environment.
See `#help cat` for more information.
-/
macro "#help" tk: ?m.132239
tk:&: String → Bool → ParserDescr
&"tactic" more: ?m.132226
more:"+"? id: ?m.132210
id:(ident: Parser.Parser
ident <|> str: Parser.Parser
str)? : command: Parser.Category
command => do
  `(#help cat$[+%$more: TSyntax Name.anonymous
more]? $(mkIdentFrom: Syntax → Name → optParam Bool false → Ident
mkIdentFrom tk: ?m.132239
tk `tactic: Name
`tactic) $(id: ?m.132210
id.map: {α : Type ?u.132759} → {β : Type ?u.132758} → (α → β) → Option α → Option β
map (⟨·.raw: {ks : SyntaxNodeKinds} → TSyntax ks → Syntax
raw⟩))?)

/--
The command `#help conv` shows all tactics that have been defined in the current environment.
See `#help cat` for more information.
-/
macro "#help" tk: ?m.135581
tk:&: String → Bool → ParserDescr
&"conv" more: ?m.135568
more:"+"? id: ?m.135552
id:(ident: Parser.Parser
ident <|> str: Parser.Parser
str)? : command: Parser.Category
command =>
  `(#help cat$[+%$more: TSyntax Name.anonymous
more]? $(mkIdentFrom: Syntax → Name → optParam Bool false → Ident
mkIdentFrom tk: ?m.135581
tk `conv: Name
`conv) $(id: ?m.135552
id.map: {α : Type ?u.136077} → {β : Type ?u.136076} → (α → β) → Option α → Option β
map (⟨·.raw: {ks : SyntaxNodeKinds} → TSyntax ks → Syntax
raw⟩))?)

/--
The command `#help command` shows all commands that have been defined in the current environment.
See `#help cat` for more information.
-/
macro "#help" tk: ?m.138918
tk:&: String → Bool → ParserDescr
&"command" more: ?m.138905
more:"+"? id: ?m.138889
id:(ident: Parser.Parser
ident <|> str: Parser.Parser
str)? : command: Parser.Category
command =>
  `(#help cat$[+%$more: TSyntax Name.anonymous
more]? $(mkIdentFrom: Syntax → Name → optParam Bool false → Ident
mkIdentFrom tk: ?m.138918
tk `command: Name
`command) $(id: ?m.138889
id.map: {α : Type ?u.139414} → {β : Type ?u.139413} → (α → β) → Option α → Option β
map (⟨·.raw: {ks : SyntaxNodeKinds} → TSyntax ks → Syntax
raw⟩))?)