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

@[extern lean_internal_has_llvm_backend]

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

This function can be used to detect whether the compiler has support for generating LLVM instead of C. It is used by lake instead of the --features flag in order to avoid having to run a compiler for this every time on startup. See #2572.

@[inline]

def Lean.isGreek (c : Char) : Bool

Valid identifier names

def Lean.isLetterLike (c : Char) : Bool

@[inline]

def Lean.isNumericSubscript (c : Char) : Bool

def Lean.isSubScriptAlnum (c : Char) : Bool

@[inline]

def Lean.isIdFirst (c : Char) : Bool

@[inline]

def Lean.isIdFirstAscii (c : UInt8) : Bool

@[inline]

def Lean.isIdRest (c : Char) : Bool

@[inline]

def Lean.isIdRestAscii (c : UInt8) : Bool

def Lean.idBeginEscape : Char

def Lean.idEndEscape : Char

@[inline]

def Lean.isIdBeginEscape (c : Char) : Bool

@[inline]

def Lean.isIdEndEscape (c : Char) : Bool

def Lean.Name.getRoot : Name → Name

@[export lean_is_inaccessible_user_name]

def Lean.Name.isInaccessibleUserName : Name → Bool

Here we give a private implementation of Name.toString. The real implementation is in Init.Data.ToString.Name, which we cannot import here due to import hierarchy limitations.

The difference between the two versions is that this one uses the String.Internal.* functions, while the one in Init.Data.ToString.Name uses the public String functions. These differ in that the latter versions have better inferred borrowing annotations, which is significant for an inner-loop function like Name.toString.

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

@[implicit_reducible]

instance Lean.Name.instRepr : Repr Name

def Lean.Name.capitalize : Name → Name

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

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

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

@[inline]

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

Remove macros scopes, apply f, and put them back

@[export lean_name_append_after]

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

@[export lean_name_append_index_after]

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

@[export lean_name_append_before]

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

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

instance Lean.Name.instLawfulBEq : LawfulBEq Name

@[implicit_reducible]

instance Lean.Name.instDecidableEq : DecidableEq Name

@[inline]

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

@[inline]

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

@[inline]

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

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

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

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

Creates a globally unique Name, without any semantic interpretation. The names are not intended to be user-visible. With the default name generator, names use _uniq as a base and have a numeric suffix.

This is used for example by Lean.mkFreshFVarId, Lean.mkFreshMVarId, and Lean.mkFreshLMVarId. To create fresh user-visible identifiers, use functions such as Lean.Core.mkFreshUserName instead.

@[implicit_reducible]

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

def Lean.Syntax.instReprPreresolved.repr : Preresolved → Nat → Std.Format

@[implicit_reducible]

instance Lean.Syntax.instReprPreresolved : Repr Preresolved

@[implicit_reducible]

instance Lean.Syntax.instRepr : Repr Syntax

partial def Lean.Syntax.instRepr.repr : Syntax → Nat → Std.Format

@[implicit_reducible]

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

def Lean.Syntax.instReprTSyntax.repr {ks✝ : SyntaxNodeKinds} : TSyntax ks✝ → Nat → Std.Format

@[reducible, inline]

abbrev Lean.Syntax.Term : Type

Syntax that represents a Lean term.

@[reducible, inline]

abbrev Lean.Syntax.Command : Type

Syntax that represents a command.

@[reducible, inline]

abbrev Lean.Syntax.Level : Type

Syntax that represents a universe level.

@[reducible, inline]

abbrev Lean.Syntax.Tactic : Type

Syntax that represents a tactic.

@[reducible, inline]

abbrev Lean.Syntax.Prec : Type

Syntax that represents a precedence (e.g. for an operator).

@[reducible, inline]

abbrev Lean.Syntax.Prio : Type

Syntax that represents a priority (e.g. for an instance declaration).

@[reducible, inline]

abbrev Lean.Syntax.Ident : Type

Syntax that represents an identifier.

@[reducible, inline]

abbrev Lean.Syntax.StrLit : Type

Syntax that represents a string literal.

@[reducible, inline]

abbrev Lean.Syntax.CharLit : Type

Syntax that represents a character literal.

@[reducible, inline]

abbrev Lean.Syntax.NameLit : Type

Syntax that represents a quoted name literal that begins with a back-tick.

@[reducible, inline]

abbrev Lean.Syntax.ScientificLit : Type

Syntax that represents a scientific numeric literal that may have decimal and exponential parts.

@[reducible, inline]

abbrev Lean.Syntax.NumLit : Type

Syntax that represents a numeric literal.

@[reducible, inline]

abbrev Lean.Syntax.HygieneInfo : Type

Syntax that represents macro hygiene info.

@[reducible, inline]

abbrev Lean.Syntax.HexNum : Type

Syntax that represent a hexadecimal number without the 0x prefix.

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.TSyntax.instCoeIdentTerm : Coe Ident Term

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.TSyntax.instCoeStrLitTerm : Coe StrLit Term

@[implicit_reducible]

instance Lean.TSyntax.instCoeNameLitTerm : Coe NameLit Term

@[implicit_reducible]

instance Lean.TSyntax.instCoeScientificLitTerm : Coe ScientificLit Term

@[implicit_reducible]

instance Lean.TSyntax.instCoeNumLitTerm : Coe NumLit Term

@[implicit_reducible]

instance Lean.TSyntax.instCoeCharLitTerm : Coe CharLit Term

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.TSyntax.instCoeNumLitPrio : Coe NumLit Prio

@[implicit_reducible]

instance Lean.TSyntax.instCoeNumLitPrec : Coe NumLit Prec

@[implicit_reducible]

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

@[implicit_reducible]

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

def Lean.Syntax.instBEqPreresolved.beq : Preresolved → Preresolved → Bool

@[implicit_reducible]

instance Lean.Syntax.instBEqPreresolved : BEq Preresolved

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

Compare syntax structures modulo source info.

@[implicit_reducible]

instance Lean.Syntax.instBEq : BEq Syntax

@[implicit_reducible]

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

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

Finds the first SourceInfo from the back of stx or none if no SourceInfo can be found.

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

Finds the first SourceInfo from the back of stx or SourceInfo.none if no SourceInfo can be found.

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

Finds the trailing size of the first SourceInfo from the back of stx. If no SourceInfo can be found or the first SourceInfo from the back of stx contains no trailing whitespace, the result is 0.

def Lean.Syntax.getTrailing? (stx : Syntax) : Option Substring.Raw

Finds the trailing whitespace substring of the first SourceInfo from the back of stx. If no SourceInfo can be found or the first SourceInfo from the back of stx contains no trailing whitespace, the result is none.

def Lean.Syntax.getTrailingTailPos? (stx : Syntax) (canonicalOnly : Bool := false) : Option String.Pos.Raw

Finds the tail position of the trailing whitespace of the first SourceInfo from the back of stx. If no SourceInfo can be found or the first SourceInfo from the back of stx contains no trailing whitespace and lacks a tail position, the result is none.

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

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 : SourceInfo) : Syntax → Option Syntax

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

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

Replaces the trailing whitespace in stx, if any, with an empty substring.

The trailing substring's startPos and str are preserved in order to ensure that the result could have been produced by the parser, in case any syntax consumers rely on such an assumption.

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

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

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

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

Return the first atom/identifier that has position information

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

def Lean.Syntax.mkSynthetic (stx : Syntax) : 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] [MonadRef m] {α : Type} (x : m α) : m α

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

partial def Lean.expandMacros (stx : Syntax) (p : SyntaxNodeKind → Bool := fun (k : SyntaxNodeKind) => k != `Lean.Parser.Term.byTactic) : MacroM 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 syntactic categories are expanded by expandMacros.

Helper functions for processing Syntax programmatically

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

Creates an identifier with its position copied from src.

To refer to a specific constant without a risk of variable capture, use mkCIdentFrom instead.

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

Creates an identifier with its position copied from the syntax returned by getRef.

To refer to a specific constant without a risk of variable capture, use mkCIdentFromRef instead.

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

Creates an identifier referring to a constant c. The identifier's position is copied from src.

This variant of mkIdentFrom makes sure that the identifier cannot accidentally be captured.

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

Creates an identifier referring to a constant c. The identifier's position is copied from the syntax returned by getRef.

This variant of mkIdentFrom makes sure that the identifier cannot accidentally be captured.

def Lean.mkCIdent (c : Name) : Ident

Creates an identifier that refers to a constant c. The identifier has no source position.

This variant of mkIdent makes sure that the identifier cannot accidentally be captured.

@[export lean_mk_syntax_ident]

def Lean.mkIdent (val : Name) : Ident

Creates an identifier from a name. The resulting identifier has no source position.

@[inline]

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

Creates a group node, as if it were parsed by Lean.Parser.group.

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

Creates an array of syntax, separated by sep.

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

Creates an optional node.

Optional nodes consist of null nodes that contain either zero or one element.

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

Creates a hole (_). The hole's position is copied from ref.

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

Creates the syntax of a separated array of items. sep is inserted between each item from a, and the result is wrapped in a null node.

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

Constructs a typed separated array from elements by adding suitable separators. The provided array should not include the separators.

Like Syntax.TSepArray.ofElems but for untyped syntax.

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

Constructs a typed separated array from elements by adding suitable separators. The provided array should not include the separators. The generated separators' source location is that of the syntax returned by getRef.

@[implicit_reducible]

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

def Lean.Syntax.TSepArray.ofElems {k : SyntaxNodeKinds} {sep : String} (elems : Array (TSyntax k)) : TSepArray k sep

Constructs a typed separated array from elements by adding suitable separators. The provided array should not include the separators.

Like Syntax.SepArray.ofElems but for typed syntax.

@[implicit_reducible]

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

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

Creates syntax representing a Lean term application, but avoids degenerate empty applications.

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

Creates syntax representing a Lean constant application, but avoids degenerate empty applications.

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

Creates a literal of the given kind. It is the caller's responsibility to ensure that the provided literal is a valid atom for the provided kind.

If info is provided, then the literal's source information is copied from it.

def Lean.Syntax.mkCharLit (val : Char) (info : SourceInfo := SourceInfo.none) : CharLit

Creates literal syntax for the given character.

If info is provided, then the literal's source information is copied from it.

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

Creates literal syntax for the given string.

If info is provided, then the literal's source information is copied from it.

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

Creates literal syntax for a number, which is provided as a string. The caller must ensure that the string is a valid token for the num token parser.

If info is provided, then the literal's source information is copied from it.

def Lean.Syntax.mkNatLit (val : Nat) (info : SourceInfo := SourceInfo.none) : NumLit

Creates literal syntax for a natural number.

If info is provided, then the literal's source information is copied from it.

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

Creates literal syntax for a number in scientific notation. The caller must ensure that the provided string is a valid scientific notation literal.

If info is provided, then the literal's source information is copied from it.

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

Creates literal syntax for a name. The caller must ensure that the provided string is a valid name literal.

If info is provided, then the literal's source information is copied from it.

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 : SyntaxNodeKind) (stx : Syntax) : Option String

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

def Lean.Syntax.isFieldIdx? (s : 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.

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

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

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

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

def Lean.Syntax.decodeStringGap (s : String) (i : String.Pos.Raw) : Option String.Pos.Raw

Decodes a valid string gap after the \. Note that this function matches "\" whitespace+ rather than the more restrictive "\" newline whitespace* since this simplifies the implementation. Justification: this does not overlap with any other sequences beginning with \.

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

partial def Lean.Syntax.decodeRawStrLitAux (s : String) (i : String.Pos.Raw) (num : Nat) : String

Takes a raw string literal, counts the number of #'s after the r, and interprets it as a string. The position i should start at 1, which is the character after the leading r. The algorithm is simple: we are given r##...#"...string..."##...# with zero or more #s. By counting the number of leading #'s, we can extract the ...string....

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

Takes the string literal lexical syntax parsed by the parser and interprets it as a string. This is where escape sequences are processed for example. The string s is either a plain string literal or a raw string literal.

If it returns none then the string literal is ill-formed, which indicates a bug in the parser. The function is not required to return none if the string literal is ill-formed.

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

If the provided Syntax is a string literal, returns the string it represents.

Even if the Syntax is a str node, the function may return none if its internally ill-formed. The parser should always create well-formed str nodes.

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

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

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

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.Raw.toName (s : Raw) : Lean.Name

Converts a substring to the Lean compiler's representation of names. The resulting name is hierarchical, and the string is split at the dots ('.').

"a.b".toRawSubstring.toName is the name a.b, not «a.b». For the latter, use Name.mkSimple ∘ Substring.Raw.toString. -- TODO: deprecate old name

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

Converts a string to the Lean compiler's representation of names. The resulting name is hierarchical, and the string is split at the dots ('.').

"a.b".toName is the name a.b, not «a.b». For the latter, use Name.mkSimple.

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

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

def Lean.Syntax.hasArgs : Syntax → Bool

def Lean.Syntax.isAtom : Syntax → Bool

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

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

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

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

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

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

Interprets a numeric literal as a natural number.

Returns 0 if the syntax is malformed.

def Lean.TSyntax.getHexNumVal (s : Syntax.HexNum) : Nat

Returns the value of the hexadecimal numeral as a natural number.

def Lean.TSyntax.getHexNumSize (s : Syntax.HexNum) : Nat

Returns the number of hexadecimal digits.

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

Extracts the parsed name from the syntax of an identifier.

Returns Name.anonymous if the syntax is malformed.

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

Extracts the components of a scientific numeric literal.

Returns a triple (n, sign, e) : Nat × Bool × Nat; the number's value is given by:

if sign then n * 10 ^ (-e) else n * 10 ^ e

Returns (0, false, 0) if the syntax is malformed.

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

Decodes a string literal, removing quotation marks and unescaping escaped characters.

Returns "" if the syntax is malformed.

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

Decodes a character literal.

Returns (default : Char) if the syntax is malformed.

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

Decodes a quoted name literal, returning the name.

Returns Lean.Name.anonymous if the syntax is malformed.

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

Decodes macro hygiene information.

@[implicit_reducible]

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

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

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

Converts a runtime value into surface syntax that denotes it.

Instances do not need to guarantee that the resulting syntax will always re-elaborate into an equivalent value. For example, the syntax may omit implicit arguments that can usually be found automatically.

• quote : α → TSyntax k

  Returns syntax for the given value.

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.instQuoteTermMkStr1 : Quote Term

@[implicit_reducible]

instance Lean.instQuoteBoolMkStr1 : Quote Bool

@[implicit_reducible]

instance Lean.instQuoteCharCharLitKind : Quote Char charLitKind

@[implicit_reducible]

instance Lean.instQuoteStringStrLitKind : Quote String strLitKind

@[implicit_reducible]

instance Lean.instQuoteNatNumLitKind : Quote Nat numLitKind

@[implicit_reducible]

instance Lean.instQuoteRawMkStr1 : Quote Substring.Raw

def Lean.quoteNameMk : Name → Term

@[implicit_reducible]

instance Lean.instQuoteNameMkStr1 : Quote Name

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

Evaluator for prec DSL

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

Evaluator for prio DSL

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

@[reducible, inline]

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)

Filters an array of syntax, treating every other element as a separator rather than an element to test with the monadic predicate p. The resulting array contains the tested elements for which p returns true, separated by the corresponding separator elements.

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

Filters an array of syntax, treating every other element as a separator rather than an element to test with the predicate p. The resulting array contains the tested elements for which p returns true, separated by the corresponding separator elements.

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 : SepArray sep) : Array Syntax

Extracts the non-separator elements of a separated array.

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

Extracts the non-separator elements of a separated array.

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

Adds an element to the end of a separated array, adding a separator as needed.

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

Helper functions for manipulating interpolated strings

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

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

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

def Lean.TSyntax.expandInterpolatedStr (interpStr : TSyntax interpolatedStrKind) (type ofInterpFn : Term) (ofLitFn : Term := ofInterpFn) : MacroM Term

Expand interpStr into a term of type type (which supports ++), calling ofInterpFn on terms within {}, and ofLitFn on the literals between the interpolations.

def Lean.TSyntax.getDocString (stx : TSyntax `Lean.Parser.Command.docComment) : String

@[implicit_reducible]

instance Lean.Meta.instReprTransparencyMode : Repr TransparencyMode

def Lean.Meta.instReprTransparencyMode.repr : TransparencyMode → Nat → Std.Format

def Lean.Meta.instReprConfig.repr : DSimp.Config → Nat → Std.Format

def Lean.Meta.instReprConfig_1.repr : Simp.Config → Nat → Std.Format

@[implicit_reducible]

instance Lean.Meta.instReprConfig_1 : Repr Simp.Config

@[implicit_reducible]

instance Lean.Meta.instReprEtaStructMode : Repr EtaStructMode

@[implicit_reducible]

instance Lean.Meta.instReprConfig : Repr DSimp.Config

def Lean.Meta.instReprEtaStructMode.repr : EtaStructMode → Nat → Std.Format

def Lean.Meta.Occurrences.contains : Occurrences → Nat → Bool

def Lean.Meta.Occurrences.isAll : Occurrences → Bool

inductive Lean.Meta.ApplyNewGoals : Type

Controls which new mvars are turned in to goals by the apply tactic.

• nonDependentFirst mvars that don't depend on other goals appear first in the goal list.
• nonDependentOnly only mvars that don't depend on other goals are added to goal list.
• all all unassigned mvars are added to the goal list.

• nonDependentFirst : ApplyNewGoals
• nonDependentOnly : ApplyNewGoals
• all : ApplyNewGoals

structure Lean.Meta.ApplyConfig : Type

Configures the behaviour of the apply tactic.

• newGoals : ApplyNewGoals
• synthAssignedInstances : Bool

  If synthAssignedInstances is true, then apply will synthesize instance implicit arguments even if they have assigned by isDefEq, and then check whether the synthesized value matches the one inferred. The congr tactic sets this flag to false.

• allowSynthFailures : Bool

  If allowSynthFailures is true, then apply will return instance implicit arguments for which typeclass search failed as new goals.

• approx : Bool

  If approx := true, then we turn on isDefEq approximations. That is, we use the approxDefEq combinator.

@[reducible, inline]

abbrev Lean.Meta.Rewrite.NewGoals : Type

Controls which new mvars are turned in to goals by the apply tactic.

• nonDependentFirst mvars that don't depend on other goals appear first in the goal list.
• nonDependentOnly only mvars that don't depend on other goals are added to goal list.
• all all unassigned mvars are added to the goal list.

structure Lean.Meta.Rewrite.Config : Type

Configures the behavior of the rewrite and rw tactics.

• transparency : TransparencyMode

  The transparency mode to use for unfolding

• offsetCnstrs : Bool

  Whether to support offset constraints such as ?x + 1 =?= e

• occs : Occurrences

  Which occurrences to rewrite

• newGoals : NewGoals

  How to convert the resulting metavariables into new goals

structure Lean.Meta.Omega.OmegaConfig : Type

Configures the behaviour of the omega tactic.

• splitDisjunctions : Bool

  Split disjunctions in the context.

  Note that with splitDisjunctions := false omega will not be able to solve x = y goals as these are usually handled by introducing ¬ x = y as a hypothesis, then replacing this with x < y ∨ x > y.

  On the other hand, omega does not currently detect disjunctions which, when split, introduce no new useful information, so the presence of irrelevant disjunctions in the context can significantly increase run time.

• splitNatSub : Bool

  Whenever ((a - b : Nat) : Int) is found, register the disjunction b ≤ a ∧ ((a - b : Nat) : Int) = a - b ∨ a < b ∧ ((a - b : Nat) : Int) = 0 for later splitting.

• splitNatAbs : Bool

  Whenever Int.natAbs a is found, register the disjunction 0 ≤ a ∧ Int.natAbs a = a ∨ a < 0 ∧ Int.natAbs a = - a for later splitting.

• splitMinMax : Bool

  Whenever min a b or max a b is found, rewrite in terms of the definition if a ≤ b ..., for later case splitting.

inductive Lean.Meta.CheckTactic.CheckGoalType {α : Sort u} (val : α) : Prop

Type used to lift an arbitrary value into a type parameter so it can appear in a proof goal.

It is used by the #check_tactic command.

• intro {α : Sort u} (val : α) : CheckGoalType val

partial def Lean.Parser.Tactic.getConfigItems (c : Syntax) : TSyntaxArray `Lean.Parser.Tactic.configItem

Extracts the items from a tactic configuration, either a Lean.Parser.Tactic.optConfig, Lean.Parser.Tactic.config, or these wrapped in null nodes.

def Lean.Parser.Tactic.mkOptConfig (items : TSyntaxArray `Lean.Parser.Tactic.configItem) : TSyntax `Lean.Parser.Tactic.optConfig

def Lean.Parser.Tactic.appendConfig (cfg cfg' : Syntax) : TSyntax `Lean.Parser.Tactic.optConfig

Appends two tactic configurations. The configurations can be Lean.Parser.Tactic.optConfig, Lean.Parser.Tactic.config, or these wrapped in null nodes (for example because the syntax is (config)?).