def Lean.version.major : Nat

def Lean.version.minor : Nat

def Lean.version.patch : Nat

@[extern lean_get_githash]

opaque Lean.getGithash (u : Unit) : String

def Lean.githash : String

@[extern lean_version_get_is_release]

opaque Lean.version.getIsRelease (u : Unit) : Bool

def Lean.version.isRelease : Bool

@[extern lean_version_get_special_desc]

opaque Lean.version.getSpecialDesc (u : Unit) : String

Additional version description like "nightly-2018-03-11"

def Lean.version.specialDesc : String

def Lean.versionStringCore : String

def Lean.versionString : String

def Lean.origin : String

def Lean.toolchain : String

@[extern lean_internal_is_stage0]

opaque Lean.Internal.isStage0 (u : Unit) : Bool

def Lean.isGreek (c : Char) : Bool

Valid identifier names

def Lean.isLetterLike (c : Char) : Bool

def Lean.isNumericSubscript (c : Char) : Bool

def Lean.isSubScriptAlnum (c : Char) : Bool

def Lean.isIdFirst (c : Char) : Bool

def Lean.isIdRest (c : Char) : Bool

def Lean.idBeginEscape : Char

def Lean.idEndEscape : Char

def Lean.isIdBeginEscape (c : Char) : Bool

def Lean.isIdEndEscape (c : Char) : Bool

def Lean.Name.getRoot : Lake.Name → Lake.Name

Equations

• Lean.Name.getRoot Lean.Name.anonymous = Lean.Name.anonymous
• Lean.Name.getRoot (Lean.Name.str Lean.Name.anonymous str) = Lean.Name.str Lean.Name.anonymous str
• Lean.Name.getRoot (Lean.Name.num Lean.Name.anonymous i) = Lean.Name.num Lean.Name.anonymous i
• Lean.Name.getRoot (Lean.Name.str n str) = Lean.Name.getRoot n
• Lean.Name.getRoot (Lean.Name.num n i) = Lean.Name.getRoot n

@[export lean_is_inaccessible_user_name]

def Lean.Name.isInaccessibleUserName : Lake.Name → Bool

Equations

• Lean.Name.isInaccessibleUserName (Lean.Name.str pre s) = (String.contains s (Char.ofNat 10013) || s == "_inaccessible")
• Lean.Name.isInaccessibleUserName (Lean.Name.num p i) = Lean.Name.isInaccessibleUserName p
• Lean.Name.isInaccessibleUserName x = false

def Lean.Name.escapePart (s : String) : Option String

def Lean.Name.toStringWithSep (sep : String) (escape : Bool) : Lake.Name → String

Equations

• Lean.Name.toStringWithSep sep escape Lean.Name.anonymous = "[anonymous]"
• Lean.Name.toStringWithSep sep escape (Lean.Name.str Lean.Name.anonymous s) = Lean.Name.toStringWithSep.maybeEscape escape s
• Lean.Name.toStringWithSep sep escape (Lean.Name.num Lean.Name.anonymous v) = toString v
• Lean.Name.toStringWithSep sep escape (Lean.Name.str n s) = Lean.Name.toStringWithSep sep escape n ++ sep ++ Lean.Name.toStringWithSep.maybeEscape escape s
• Lean.Name.toStringWithSep sep escape (Lean.Name.num n v) = Lean.Name.toStringWithSep sep escape n ++ sep ++ Nat.repr v

def Lean.Name.toStringWithSep.maybeEscape (escape : Bool) (s : String) : String

def Lean.Name.toString (n : Lake.Name) (escape : optParam Bool true) : String

def Lean.Name.toString.maybePseudoSyntax (n : Lake.Name) : Bool

instance Lean.Name.instToStringName : ToString Lake.Name

def Lean.Name.reprPrec (n : Lake.Name) (prec : Nat) : Lean.Format

Equations

• One or more equations did not get rendered due to their size.
• Lean.Name.reprPrec Lean.Name.anonymous prec = Std.Format.text "Lean.Name.anonymous"
• Lean.Name.reprPrec (Lean.Name.num pre i) prec = Repr.addAppParen (Std.Format.text "Lean.Name.mkNum " ++ Lean.Name.reprPrec pre 1024 ++ Std.Format.text " " ++ repr i) prec

instance Lean.Name.instReprName : Repr Lake.Name

def Lean.Name.capitalize : Lake.Name → Lake.Name

def Lean.Name.replacePrefix : Lake.Name → Lake.Name → Lake.Name → Lake.Name

Equations

• Lean.Name.replacePrefix Lean.Name.anonymous Lean.Name.anonymous x = x
• Lean.Name.replacePrefix Lean.Name.anonymous x x = Lean.Name.anonymous
• Lean.Name.replacePrefix (Lean.Name.str p s) x x = if (Lean.Name.str p s == x) = true then x else Lean.Name.mkStr (Lean.Name.replacePrefix p x x) s
• Lean.Name.replacePrefix (Lean.Name.num p s) x x = if (Lean.Name.num p s == x) = true then x else Lean.Name.mkNum (Lean.Name.replacePrefix p x x) s

def Lean.Name.eraseSuffix? : Lake.Name → Lake.Name → Option Lake.Name

eraseSuffix? n s return n' if n is of the form n == n' ++ s.

@[inline]

def Lean.Name.modifyBase (n : Lake.Name) (f : Lake.Name → Lake.Name) : Lake.Name

Remove macros scopes, apply f, and put them back

@[export lean_name_append_after]

def Lean.Name.appendAfter (n : Lake.Name) (suffix : String) : Lake.Name

@[export lean_name_append_index_after]

def Lean.Name.appendIndexAfter (n : Lake.Name) (idx : Nat) : Lake.Name

@[export lean_name_append_before]

def Lean.Name.appendBefore (n : Lake.Name) (pre : String) : Lake.Name

theorem Lean.Name.beq_iff_eq {m : Lake.Name} {n : Lake.Name} : (m == n) = true ↔ m = n

instance Lean.Name.instLawfulBEqNameInstBEqName : LawfulBEq Lake.Name

instance Lean.Name.instDecidableEqName : DecidableEq Lake.Name

structure Lean.NameGenerator : Type

• namePrefix : Lake.Name
• idx : Nat

instance Lean.instInhabitedNameGenerator : Inhabited Lean.NameGenerator

@[inline]

def Lean.NameGenerator.curr (g : Lean.NameGenerator) : Lake.Name

@[inline]

def Lean.NameGenerator.next (g : Lean.NameGenerator) : Lean.NameGenerator

@[inline]

def Lean.NameGenerator.mkChild (g : Lean.NameGenerator) : Lean.NameGenerator × Lean.NameGenerator

class Lean.MonadNameGenerator (m : Type → Type) : Type

• getNGen : m Lean.NameGenerator
• setNGen : Lean.NameGenerator → m Unit

def Lean.mkFreshId {m : Type → Type} [Monad m] [Lean.MonadNameGenerator m] : m Lake.Name

instance Lean.monadNameGeneratorLift (m : Type → Type) (n : Type → Type) [MonadLift m n] [Lean.MonadNameGenerator m] : Lean.MonadNameGenerator n

instance Lean.Syntax.instReprPreresolved : Repr Lean.Syntax.Preresolved

instance Lean.Syntax.instReprSyntax : Repr Lean.Syntax

instance Lean.Syntax.instReprTSyntax : {ks : Lean.SyntaxNodeKinds} → Repr (Lean.TSyntax ks)

@[inline, reducible]

abbrev Lean.Syntax.Term : Type

@[inline, reducible]

abbrev Lean.Syntax.Command : Type

@[inline, reducible]

abbrev Lean.Syntax.Level : Type

@[inline, reducible]

abbrev Lean.Syntax.Tactic : Type

@[inline, reducible]

abbrev Lean.Syntax.Prec : Type

@[inline, reducible]

abbrev Lean.Syntax.Prio : Type

@[inline, reducible]

abbrev Lean.Syntax.Ident : Type

@[inline, reducible]

abbrev Lean.Syntax.StrLit : Type

@[inline, reducible]

abbrev Lean.Syntax.CharLit : Type

@[inline, reducible]

abbrev Lean.Syntax.NameLit : Type

@[inline, reducible]

abbrev Lean.Syntax.ScientificLit : Type

@[inline, reducible]

abbrev Lean.Syntax.NumLit : Type

@[inline, reducible]

abbrev Lean.Syntax.HygieneInfo : Type

instance Lean.TSyntax.instCoeTSyntaxConsSyntaxNodeKindNil {k : Lean.SyntaxNodeKind} {ks : List Lean.SyntaxNodeKind} : Coe (Lean.TSyntax k) (Lean.TSyntax (k :: ks))

instance Lean.TSyntax.instCoeTSyntaxConsSyntaxNodeKind {ks : Lean.SyntaxNodeKinds} {k' : Lean.SyntaxNodeKind} : Coe (Lean.TSyntax ks) (Lean.TSyntax (k' :: ks))

instance Lean.TSyntax.instCoeIdentTerm : Coe Lean.Ident Lean.Term

instance Lean.TSyntax.instCoeDepTermMkConsSyntaxNodeKindMkStr1NilIdentIdent {info : Lean.SourceInfo} {ss : Substring} {n : Lake.Name} {res : List Lean.Syntax.Preresolved} : CoeDep Lean.Term { raw := Lean.Syntax.ident info ss n res } Lean.Ident

instance Lean.TSyntax.instCoeStrLitTerm : Coe Lean.StrLit Lean.Term

instance Lean.TSyntax.instCoeNameLitTerm : Coe Lean.NameLit Lean.Term

instance Lean.TSyntax.instCoeScientificLitTerm : Coe Lean.ScientificLit Lean.Term

instance Lean.TSyntax.instCoeNumLitTerm : Coe Lean.NumLit Lean.Term

instance Lean.TSyntax.instCoeCharLitTerm : Coe Lean.CharLit Lean.Term

instance Lean.TSyntax.instCoeIdentLevel : Coe Lean.Ident Lean.Syntax.Level

instance Lean.TSyntax.instCoeNumLitPrio : Coe Lean.NumLit Lean.Prio

instance Lean.TSyntax.instCoeNumLitPrec : Coe Lean.NumLit Lean.Prec

def Lean.TSyntax.Compat.instCoeTailSyntaxTSyntax {k : Lean.SyntaxNodeKinds} : CoeTail Lean.Syntax (Lean.TSyntax k)

def Lean.TSyntax.Compat.instCoeTailArraySyntaxTSyntaxArray {k : Lean.SyntaxNodeKinds} : CoeTail (Array Lean.Syntax) (Lean.TSyntaxArray k)

instance Lean.Syntax.instBEqPreresolved : BEq Lean.Syntax.Preresolved

partial def Lean.Syntax.structEq : Lean.Syntax → Lean.Syntax → Bool

Compare syntax structures modulo source info.

instance Lean.Syntax.instBEqSyntax : BEq Lean.Syntax

instance Lean.Syntax.instBEqTSyntax {k : Lean.SyntaxNodeKinds} : BEq (Lean.TSyntax k)

partial def Lean.Syntax.getTailInfo? : Lean.Syntax → Option Lean.SourceInfo

def Lean.Syntax.getTailInfo (stx : Lean.Syntax) : Lean.SourceInfo

def Lean.Syntax.getTrailingSize (stx : Lean.Syntax) : Nat

def Lean.Syntax.getSubstring? (stx : Lean.Syntax) (withLeading : optParam Bool true) (withTrailing : optParam Bool true) : Option Substring

Return substring of original input covering stx. Result is meaningful only if all involved SourceInfo.originals refer to the same string (as is the case after parsing).

partial def Lean.Syntax.setTailInfoAux (info : Lean.SourceInfo) : Lean.Syntax → Option Lean.Syntax

def Lean.Syntax.setTailInfo (stx : Lean.Syntax) (info : Lean.SourceInfo) : Lean.Syntax

def Lean.Syntax.unsetTrailing (stx : Lean.Syntax) : Lean.Syntax

partial def Lean.Syntax.setHeadInfoAux (info : Lean.SourceInfo) : Lean.Syntax → Option Lean.Syntax

def Lean.Syntax.setHeadInfo (stx : Lean.Syntax) (info : Lean.SourceInfo) : Lean.Syntax

def Lean.Syntax.setInfo (info : Lean.SourceInfo) : Lean.Syntax → Lean.Syntax

partial def Lean.Syntax.getHead? : Lean.Syntax → Option Lean.Syntax

Return the first atom/identifier that has position information

def Lean.Syntax.copyHeadTailInfoFrom (target : Lean.Syntax) (source : Lean.Syntax) : Lean.Syntax

def Lean.Syntax.mkSynthetic (stx : Lean.Syntax) : Lean.Syntax

Ensure head position is synthetic. The server regards syntax as "original" only if both head and tail info are original.

@[inline]

def Lean.withHeadRefOnly {m : Type → Type} [Monad m] [Lean.MonadRef m] {α : Type} (x : m α) : m α

Use the head atom/identifier of the current ref as the ref

structure Lean.Module : Type

• header : Lean.Syntax
• commands : Array Lean.Syntax

Syntax objects for a Lean module.

partial def Lean.expandMacros (stx : Lean.Syntax) (p : optParam (Lean.SyntaxNodeKind → Bool) fun k => k != `Lean.Parser.Term.byTactic) : Lean.MacroM Lean.Syntax

Expand macros in the given syntax. A node with kind k is visited only if p k is true.

Note that the default value for p returns false for by ... nodes. This is a "hack". The tactic framework abuses the macro system to implement extensible tactics. For example, one can define

syntax "my_trivial" : tactic -- extensible tactic

macro_rules | `(tactic| my_trivial) => `(tactic| decide)
macro_rules | `(tactic| my_trivial) => `(tactic| assumption)

When the tactic evaluator finds the tactic my_trivial, it tries to evaluate the macro_rule expansions until one "works", i.e., the macro expansion is evaluated without producing an exception. We say this solution is a bit hackish because the term elaborator may invoke expandMacros with (p := fun _ => true), and expand the tactic macros as just macros. In the example above, my_trivial would be replaced with assumption, decide would not be tried if assumption fails at tactic evaluation time.

We are considering two possible solutions for this issue: 1- A proper extensible tactic feature that does not rely on the macro system.

2- Typed macros that know the syntax categories they're working in. Then, we would be able to select which syntatic categories are expanded by expandMacros.

Helper functions for processing Syntax programmatically

def Lean.mkIdentFrom (src : Lean.Syntax) (val : Lake.Name) (canonical : optParam Bool false) : Lean.Ident

Create an identifier copying the position from src. To refer to a specific constant, use mkCIdentFrom instead.

def Lean.mkIdentFromRef {m : Type → Type} [Monad m] [Lean.MonadRef m] (val : Lake.Name) (canonical : optParam Bool false) : m Lean.Ident

def Lean.mkCIdentFrom (src : Lean.Syntax) (c : Lake.Name) (canonical : optParam Bool false) : Lean.Ident

Create an identifier referring to a constant c copying the position from src. This variant of mkIdentFrom makes sure that the identifier cannot accidentally be captured.

def Lean.mkCIdentFromRef {m : Type → Type} [Monad m] [Lean.MonadRef m] (c : Lake.Name) (canonical : optParam Bool false) : m Lean.Syntax

def Lean.mkCIdent (c : Lake.Name) : Lean.Ident

@[export lean_mk_syntax_ident]

def Lean.mkIdent (val : Lake.Name) : Lean.Ident

@[inline]

def Lean.mkGroupNode (args : optParam (Array Lean.Syntax) #[]) : Lean.Syntax

def Lean.mkSepArray (as : Array Lean.Syntax) (sep : Lean.Syntax) : Array Lean.Syntax

def Lean.mkOptionalNode (arg : Option Lean.Syntax) : Lean.Syntax

def Lean.mkHole (ref : Lean.Syntax) (canonical : optParam Bool false) : Lean.Syntax

def Lean.Syntax.mkSep (a : Array Lean.Syntax) (sep : Lean.Syntax) : Lean.Syntax

def Lean.Syntax.SepArray.ofElems {sep : String} (elems : Array Lean.Syntax) : Lean.Syntax.SepArray sep

def Lean.Syntax.SepArray.ofElemsUsingRef {m : Type → Type} [Monad m] [Lean.MonadRef m] {sep : String} (elems : Array Lean.Syntax) : m (Lean.Syntax.SepArray sep)

instance Lean.Syntax.instCoeArraySyntaxSepArray {sep : String} : Coe (Array Lean.Syntax) (Lean.Syntax.SepArray sep)

instance Lean.Syntax.instCoeTSyntaxArrayTSepArray {k : Lean.SyntaxNodeKinds} {sep : String} : Coe (Lean.TSyntaxArray k) (Lean.Syntax.TSepArray k sep)

def Lean.Syntax.mkApp (fn : Lean.Term) (args : Lean.TSyntaxArray `term) : Lean.Term

Create syntax representing a Lean term application, but avoid degenerate empty applications.

def Lean.Syntax.mkCApp (fn : Lake.Name) (args : Lean.TSyntaxArray `term) : Lean.Term

def Lean.Syntax.mkLit (kind : Lean.SyntaxNodeKind) (val : String) (info : optParam Lean.SourceInfo Lean.SourceInfo.none) : Lean.TSyntax kind

def Lean.Syntax.mkStrLit (val : String) (info : optParam Lean.SourceInfo Lean.SourceInfo.none) : Lean.StrLit

def Lean.Syntax.mkNumLit (val : String) (info : optParam Lean.SourceInfo Lean.SourceInfo.none) : Lean.NumLit

def Lean.Syntax.mkScientificLit (val : String) (info : optParam Lean.SourceInfo Lean.SourceInfo.none) : Lean.TSyntax Lean.scientificLitKind

def Lean.Syntax.mkNameLit (val : String) (info : optParam Lean.SourceInfo Lean.SourceInfo.none) : Lean.NameLit

Recall that we don't have special Syntax constructors for storing numeric and string atoms. The idea is to have an extensible approach where embedded DSLs may have new kind of atoms and/or different ways of representing them. So, our atoms contain just the parsed string. The main Lean parser uses the kind numLitKind for storing natural numbers that can be encoded in binary, octal, decimal and hexadecimal format. isNatLit implements a "decoder" for Syntax objects representing these numerals.

def Lean.Syntax.decodeNatLitVal? (s : String) : Option Nat

def Lean.Syntax.isLit? (litKind : Lean.SyntaxNodeKind) (stx : Lean.Syntax) : Option String

def Lean.Syntax.isNatLit? (s : Lean.Syntax) : Option Nat

def Lean.Syntax.isFieldIdx? (s : Lean.Syntax) : Option Nat

def Lean.Syntax.decodeScientificLitVal? (s : String) : Option (Nat × Bool × Nat)

Decodes a 'scientific number' string which is consumed by the OfScientific class. Takes as input a string such as 123, 123.456e7 and returns a triple (n, sign, e) with value given by n * 10^-e if sign else n * 10^e.

partial def Lean.Syntax.decodeScientificLitVal?.decodeAfterExp (s : String) (i : String.Pos) (val : Nat) (e : Nat) (sign : Bool) (exp : Nat) : Option (Nat × Bool × Nat)

def Lean.Syntax.decodeScientificLitVal?.decodeExp (s : String) (i : String.Pos) (val : Nat) (e : Nat) : Option (Nat × Bool × Nat)

partial def Lean.Syntax.decodeScientificLitVal?.decodeAfterDot (s : String) (i : String.Pos) (val : Nat) (e : Nat) : Option (Nat × Bool × Nat)

partial def Lean.Syntax.decodeScientificLitVal?.decode (s : String) (i : String.Pos) (val : Nat) : Option (Nat × Bool × Nat)

def Lean.Syntax.isScientificLit? (stx : Lean.Syntax) : Option (Nat × Bool × Nat)

def Lean.Syntax.isIdOrAtom? : Lean.Syntax → Option String

def Lean.Syntax.toNat (stx : Lean.Syntax) : Nat

def Lean.Syntax.decodeQuotedChar (s : String) (i : String.Pos) : Option (Char × String.Pos)

partial def Lean.Syntax.decodeStrLitAux (s : String) (i : String.Pos) (acc : String) : Option String

def Lean.Syntax.decodeStrLit (s : String) : Option String

def Lean.Syntax.isStrLit? (stx : Lean.Syntax) : Option String

def Lean.Syntax.decodeCharLit (s : String) : Option Char

def Lean.Syntax.isCharLit? (stx : Lean.Syntax) : Option Char

def Lean.Syntax.splitNameLit (ss : Substring) : List Substring

Split a name literal (without the backtick) into its dot-separated components. For example, foo.bla.«bo.o» ↦ ["foo", "bla", "«bo.o»"]. If the literal cannot be parsed, return [].

def Substring.toName (s : Substring) : Lake.Name

def String.toName (s : String) : Lake.Name

def Lean.Syntax.decodeNameLit (s : String) : Option Lake.Name

def Lean.Syntax.isNameLit? (stx : Lean.Syntax) : Option Lake.Name

def Lean.Syntax.hasArgs : Lean.Syntax → Bool

def Lean.Syntax.isAtom : Lean.Syntax → Bool

def Lean.Syntax.isToken (token : String) : Lean.Syntax → Bool

def Lean.Syntax.isNone (stx : Lean.Syntax) : Bool

def Lean.Syntax.getOptionalIdent? (stx : Lean.Syntax) : Option Lake.Name

partial def Lean.Syntax.findAux (p : Lean.Syntax → Bool) : Lean.Syntax → Option Lean.Syntax

def Lean.Syntax.find? (stx : Lean.Syntax) (p : Lean.Syntax → Bool) : Option Lean.Syntax

def Lean.TSyntax.getNat (s : Lean.NumLit) : Nat

def Lean.TSyntax.getId (s : Lean.Ident) : Lake.Name

def Lean.TSyntax.getScientific (s : Lean.ScientificLit) : Nat × Bool × Nat

def Lean.TSyntax.getString (s : Lean.StrLit) : String

def Lean.TSyntax.getChar (s : Lean.CharLit) : Char

def Lean.TSyntax.getName (s : Lean.NameLit) : Lake.Name

def Lean.TSyntax.getHygieneInfo (s : Lean.HygieneInfo) : Lake.Name

def Lean.TSyntax.Compat.instCoeTailArraySyntaxTSepArray {k : Lean.SyntaxNodeKinds} {sep : String} : CoeTail (Array Lean.Syntax) (Lean.Syntax.TSepArray k sep)

def Lean.HygieneInfo.mkIdent (s : Lean.HygieneInfo) (val : Lake.Name) (canonical : optParam Bool false) : Lean.Ident

class Lean.Quote (α : Type) (k : optParam Lean.SyntaxNodeKind `term) : Type

• quote : α → Lean.TSyntax k

Reflect a runtime datum back to surface syntax (best-effort).

instance Lean.instQuote {α : Type} {k : Lean.SyntaxNodeKind} {k' : Lean.SyntaxNodeKind} [Lean.Quote α k] [CoeHTCT (Lean.TSyntax k) (Lean.TSyntax k')] : Lean.Quote α k'

instance Lean.instQuoteTermMkStr1 : Lean.Quote Lean.Term

instance Lean.instQuoteBoolMkStr1 : Lean.Quote Bool

instance Lean.instQuoteStringStrLitKind : Lean.Quote String Lean.strLitKind

instance Lean.instQuoteNatNumLitKind : Lean.Quote Nat Lean.numLitKind

instance Lean.instQuoteSubstringMkStr1 : Lean.Quote Substring

def Lean.quoteNameMk : Lake.Name → Lean.Term

Equations

• Lean.quoteNameMk Lean.Name.anonymous = { raw := (Lean.mkCIdent `Lean.Name.anonymous).raw }
• Lean.quoteNameMk (Lean.Name.str p s) = Lean.Syntax.mkCApp `Lean.Name.mkStr #[Lean.quoteNameMk p, Lean.quote `term s]
• Lean.quoteNameMk (Lean.Name.num p n) = Lean.Syntax.mkCApp `Lean.Name.mkNum #[Lean.quoteNameMk p, Lean.quote `term n]

instance Lean.instQuoteNameMkStr1 : Lean.Quote Lake.Name

instance Lean.instQuoteProdMkStr1 {α : Type} {β : Type} [Lean.Quote α] [Lean.Quote β] : Lean.Quote (α × β)

instance Lean.instQuoteListMkStr1 {α : Type} [Lean.Quote α] : Lean.Quote (List α)

instance Lean.instQuoteArrayMkStr1 {α : Type} [Lean.Quote α] : Lean.Quote (Array α)

instance Lean.Option.hasQuote {α : Type} [Lean.Quote α] : Lean.Quote (Option α)

def Lean.evalPrec (stx : Lean.Syntax) : Lean.MacroM Nat

Evaluator for prec DSL

def Lean.termEval_prec_ : Lean.ParserDescr

def Lean.evalPrio (stx : Lean.Syntax) : Lean.MacroM Nat

Evaluator for prio DSL

def Lean.termEval_prio_ : Lean.ParserDescr

def Lean.evalOptPrio : Option (Lean.TSyntax `prio) → Lean.MacroM Nat

@[inline, reducible]

abbrev Array.getSepElems {α : Type u_1} (as : Array α) : Array α

def Array.filterSepElemsM {m : Type → Type} [Monad m] (a : Array Lean.Syntax) (p : Lean.Syntax → m Bool) : m (Array Lean.Syntax)

def Array.filterSepElems (a : Array Lean.Syntax) (p : Lean.Syntax → Bool) : Array Lean.Syntax

def Array.mapSepElemsM {m : Type → Type} [Monad m] (a : Array Lean.Syntax) (f : Lean.Syntax → m Lean.Syntax) : m (Array Lean.Syntax)

def Array.mapSepElems (a : Array Lean.Syntax) (f : Lean.Syntax → Lean.Syntax) : Array Lean.Syntax

def Lean.Syntax.SepArray.getElems {sep : String} (sa : Lean.Syntax.SepArray sep) : Array Lean.Syntax

def Lean.Syntax.TSepArray.getElems {k : Lean.SyntaxNodeKinds} {sep : String} (sa : Lean.Syntax.TSepArray k sep) : Lean.TSyntaxArray k

def Lean.Syntax.TSepArray.push {k : Lean.SyntaxNodeKinds} {sep : String} (sa : Lean.Syntax.TSepArray k sep) (e : Lean.TSyntax k) : Lean.Syntax.TSepArray k sep

instance Lean.Syntax.instEmptyCollectionSepArray {sep : String} : EmptyCollection (Lean.Syntax.SepArray sep)

instance Lean.Syntax.instEmptyCollectionTSepArray {sep : Lean.SyntaxNodeKinds} {k : String} : EmptyCollection (Lean.Syntax.TSepArray sep k)

instance Lean.Syntax.instCoeOutSepArrayArraySyntax {sep : String} : CoeOut (Lean.Syntax.SepArray sep) (Array Lean.Syntax)

instance Lean.Syntax.instCoeOutTSepArrayTSyntaxArray {k : Lean.SyntaxNodeKinds} {sep : String} : CoeOut (Lean.Syntax.TSepArray k sep) (Lean.TSyntaxArray k)

instance Lean.Syntax.instCoeTSyntaxArray {k : Lean.SyntaxNodeKinds} {k' : Lean.SyntaxNodeKinds} [Coe (Lean.TSyntax k) (Lean.TSyntax k')] : Coe (Lean.TSyntaxArray k) (Lean.TSyntaxArray k')

instance Lean.Syntax.instCoeOutTSyntaxArrayArraySyntax {k : Lean.SyntaxNodeKinds} : CoeOut (Lean.TSyntaxArray k) (Array Lean.Syntax)

instance Lean.Syntax.instCoeIdentTSyntaxConsSyntaxNodeKindMkStr4Nil : Coe Lean.Ident (Lean.TSyntax `Lean.Parser.Command.declId)

instance Lean.Syntax.instCoeTermTSyntaxConsSyntaxNodeKindMkStr4Nil : Coe Lean.Term (Lean.TSyntax `Lean.Parser.Term.funBinder)

@[inline, reducible]

abbrev autoParam (α : Sort u) (tactic : Lean.Syntax) : Sort u

Gadget for automatic parameter support. This is similar to the optParam gadget, but it uses the given tactic. Like optParam, this gadget only affects elaboration. For example, the tactic will not be invoked during type class resolution.

Helper functions for manipulating interpolated strings

def Lean.Syntax.isInterpolatedStrLit? (stx : Lean.Syntax) : Option String

def Lean.Syntax.getSepArgs (stx : Lean.Syntax) : Array Lean.Syntax

def Lean.TSyntax.expandInterpolatedStrChunks (chunks : Array Lean.Syntax) (mkAppend : Lean.Syntax → Lean.Syntax → Lean.MacroM Lean.Syntax) (mkElem : Lean.Syntax → Lean.MacroM Lean.Syntax) : Lean.MacroM Lean.Syntax

def Lean.TSyntax.expandInterpolatedStr (interpStr : Lean.TSyntax Lean.interpolatedStrKind) (type : Lean.Term) (toTypeFn : Lean.Term) : Lean.MacroM Lean.Term

inductive Lean.Meta.TransparencyMode : Type

• all: Lean.Meta.TransparencyMode
• default: Lean.Meta.TransparencyMode
• reducible: Lean.Meta.TransparencyMode
• instances: Lean.Meta.TransparencyMode

instance Lean.Meta.instInhabitedTransparencyMode : Inhabited Lean.Meta.TransparencyMode

instance Lean.Meta.instBEqTransparencyMode : BEq Lean.Meta.TransparencyMode

instance Lean.Meta.instReprTransparencyMode : Repr Lean.Meta.TransparencyMode

inductive Lean.Meta.EtaStructMode : Type

• all: Lean.Meta.EtaStructMode

  Enable eta for structure and classes.

• notClasses: Lean.Meta.EtaStructMode

  Enable eta only for structures that are not classes.

• none: Lean.Meta.EtaStructMode

  Disable eta for structures and classes.

instance Lean.Meta.instInhabitedEtaStructMode : Inhabited Lean.Meta.EtaStructMode

instance Lean.Meta.instBEqEtaStructMode : BEq Lean.Meta.EtaStructMode

instance Lean.Meta.instReprEtaStructMode : Repr Lean.Meta.EtaStructMode

structure Lean.Meta.DSimp.Config : Type

• zeta : Bool
• beta : Bool
• eta : Bool
• etaStruct : Lean.Meta.EtaStructMode
• iota : Bool
• proj : Bool
• decide : Bool
• autoUnfold : Bool
• failIfUnchanged : Bool

  If failIfUnchanged := true, then calls to simp, dsimp, or simp_all will fail if they do not make progress.

instance Lean.Meta.DSimp.instInhabitedConfig : Inhabited Lean.Meta.DSimp.Config

instance Lean.Meta.DSimp.instBEqConfig : BEq Lean.Meta.DSimp.Config

instance Lean.Meta.DSimp.instReprConfig : Repr Lean.Meta.DSimp.Config

def Lean.Meta.Simp.defaultMaxSteps : Nat

structure Lean.Meta.Simp.Config : Type

• maxSteps : Nat
• maxDischargeDepth : Nat
• contextual : Bool
• memoize : Bool
• singlePass : Bool
• zeta : Bool
• beta : Bool
• eta : Bool
• etaStruct : Lean.Meta.EtaStructMode
• iota : Bool
• proj : Bool
• decide : Bool
• arith : Bool
• autoUnfold : Bool
• dsimp : Bool

  If dsimp := true, then switches to dsimp on dependent arguments where there is no congruence theorem that allows simp to visit them. If dsimp := false, then argument is not visited.

• failIfUnchanged : Bool

  If failIfUnchanged := true, then calls to simp, dsimp, or simp_all will fail if they do not make progress.

instance Lean.Meta.Simp.instInhabitedConfig : Inhabited Lean.Meta.Simp.Config

instance Lean.Meta.Simp.instBEqConfig : BEq Lean.Meta.Simp.Config

instance Lean.Meta.Simp.instReprConfig : Repr Lean.Meta.Simp.Config

structure Lean.Meta.Simp.ConfigCtxextends Lean.Meta.Simp.Config : Type

def Lean.Meta.Simp.neutralConfig : Lean.Meta.Simp.Config

structure Lean.Meta.Rewrite.Config : Type

• transparency : Lean.Meta.TransparencyMode
• offsetCnstrs : Bool

def Lean.Parser.Tactic.tacticErw__ : Lean.ParserDescr

erw [rules] is a shorthand for rw (config := { transparency := .default }) [rules]. This does rewriting up to unfolding of regular definitions (by comparison to regular rw which only unfolds @[reducible] definitions).

def Lean.Parser.Tactic.simpAllKind : Lean.ParserDescr

def Lean.Parser.Tactic.dsimpKind : Lean.ParserDescr

def Lean.Parser.Tactic.declareSimpLikeTactic : Lean.ParserDescr

def Lean.Parser.Tactic.simpAutoUnfold : Lean.ParserDescr

simp! is shorthand for simp with autoUnfold := true. This will rewrite with all equation lemmas, which can be used to partially evaluate many definitions.

def Lean.Parser.Tactic.simpArith : Lean.ParserDescr

simp_arith is shorthand for simp with arith := true. This enables the use of normalization by linear arithmetic.

def Lean.Parser.Tactic.simpArithAutoUnfold : Lean.ParserDescr

simp_arith! is shorthand for simp_arith with autoUnfold := true. This will rewrite with all equation lemmas, which can be used to partially evaluate many definitions.

def Lean.Parser.Tactic.simpAllAutoUnfold : Lean.ParserDescr

simp_all! is shorthand for simp_all with autoUnfold := true. This will rewrite with all equation lemmas, which can be used to partially evaluate many definitions.

def Lean.Parser.Tactic.simpAllArith : Lean.ParserDescr

simp_all_arith combines the effects of simp_all and simp_arith.

def Lean.Parser.Tactic.simpAllArithAutoUnfold : Lean.ParserDescr

simp_all_arith! combines the effects of simp_all, simp_arith and simp!.

def Lean.Parser.Tactic.dsimpAutoUnfold : Lean.ParserDescr

dsimp! is shorthand for dsimp with autoUnfold := true. This will rewrite with all equation lemmas, which can be used to partially evaluate many definitions.