Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl.
/-
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)? : 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) 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 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
throwError
throwError "no options found (!)": ?m.1980 ?m.1981
"no options found (!)"
for (
name: String
name
, decl) in
decls: ?m.1498
decls
do let mut
msg1: ?m.2387
msg1
:= match 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 :=
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})"
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.
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)? : 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) in ← 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 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
throwError
throwError "no attributes found (!)": ?m.14000 ?m.14001
"no attributes found (!)"
for (
name: String
name
, decl) in
decls: ?m.13518
decls
do let mut
msg1: ?m.14367
msg1
:= s!"[{
name: String
name
}]: {decl.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.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)? : 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) 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 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 let mut 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
throwError
throwError "no syntax categories found (!)": ?m.36759 ?m.36760
"no syntax categories found (!)"
for (
name: String
name
, 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.
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.
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 ++
.nest: Nat β†’ MessageData β†’ MessageData
.nest
2: ?m.38157
2
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
id: ?m.44970
id
:(ident <|> str)? : 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.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.
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, _) in cat.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
(← 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) 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.
toString: Name β†’ optParam Bool true β†’ String
toString
false: Bool
false
) 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.
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 (k :
SyntaxNodeKind: Type
SyntaxNodeKind
) (msg msg1 :
MessageData: Type
MessageData
) :
CommandElabM: Type β†’ Type
CommandElabM
MessageData: Type
MessageData
:= do let mut
msg1: ?m.100333
msg1
:= 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 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 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: Type β†’ Type
KeyedDeclsAttribute
Ξ±: ?m.100878
Ξ±
) (msg :
MessageData: Type
MessageData
) :
CommandElabM: Type β†’ Type
CommandElabM
MessageData: Type
MessageData
:= do let mut
msg: ?m.100988
msg
:= msg for
e: ?m.100982
e
in attr.
getEntries: {Ξ³ : Type} β†’ KeyedDeclsAttribute Ξ³ β†’ Environment β†’ Name β†’ List (KeyedDeclsAttribute.AttributeEntry Ξ³)
getEntries
env: ?m.100315
env
k do let
x: ?m.100991
x
:=
e: ?m.100982
e
.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 ++ msg1 ++ (
.line: Format
.line
++
.line: Format
.line
:
Format: Type
Format
) for (
name: String
name
, ks) in
decls: RBMap String (Array SyntaxNodeKind) compare
decls
do for
k: ?m.103506
k
in ks do
msg: ?m.103693
msg
← 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) in rest do
msg: ?m.104277
msg
← addMsg k
msg: ?m.104163
msg
m!"syntax ... [{
mkConst: Name β†’ optParam (List Level) [] β†’ Expr
mkConst
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 <|> str)? : command => `(#help cat$[+%$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 <|> str)? : command => do `(#help cat$[+%$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 <|> str)? : command => `(#help cat$[+%$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 <|> str)? : command => `(#help cat$[+%$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
⟩))?)