def Lean.version.major : Nat

Equations

• Lean.version.major = Lean.version.getMajor✝ ()

def Lean.version.minor : Nat

Equations

• Lean.version.minor = Lean.version.getMinor✝ ()

def Lean.version.patch : Nat

Equations

• Lean.version.patch = Lean.version.getPatch✝ ()

@[extern lean_get_githash]

opaque Lean.getGithash (u : Unit) : String

def Lean.githash : String

Equations

• Lean.githash = Lean.getGithash ()

@[extern lean_version_get_is_release]

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

def Lean.version.isRelease : Bool

Equations

• Lean.version.isRelease = Lean.version.getIsRelease ()

@[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

Equations

• Lean.version.specialDesc = Lean.version.getSpecialDesc ()

def Lean.versionStringCore : String

Equations

• Lean.versionStringCore = toString Lean.version.major ++ "." ++ toString Lean.version.minor ++ "." ++ toString Lean.version.patch

def Lean.versionString : String

Equations

• One or more equations did not get rendered due to their size.

def Lean.origin : String

Equations

• Lean.origin = "leanprover/lean4"

def Lean.toolchain : String

Equations

• One or more equations did not get rendered due to their size.

@[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

Equations

• Lean.isGreek c = (decide (913 ≤ c.val) && decide (c.val ≤ 989))

def Lean.isLetterLike (c : Char) : Bool

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lean.isNumericSubscript (c : Char) : Bool

Equations

• Lean.isNumericSubscript c = (decide (8320 ≤ c.val) && decide (c.val ≤ 8329))

def Lean.isSubScriptAlnum (c : Char) : Bool

Equations

• Lean.isSubScriptAlnum c = (Lean.isNumericSubscript c || decide (8336 ≤ c.val) && decide (c.val ≤ 8348) || decide (7522 ≤ c.val) && decide (c.val ≤ 7530))

@[inline]

def Lean.isIdFirst (c : Char) : Bool

Equations

• Lean.isIdFirst c = (c.isAlpha || decide (c = '_') || Lean.isLetterLike c)

@[inline]

def Lean.isIdRest (c : Char) : Bool

Equations

• Lean.isIdRest c = (c.isAlphanum || decide (c = '_') || decide (c = ''') || c == '!' || c == '?' || Lean.isLetterLike c || Lean.isSubScriptAlnum c)

def Lean.idBeginEscape : Char

Equations

• Lean.idBeginEscape = '«'

def Lean.idEndEscape : Char

Equations

• Lean.idEndEscape = '»'

@[inline]

def Lean.isIdBeginEscape (c : Char) : Bool

Equations

• Lean.isIdBeginEscape c = decide (c = Lean.idBeginEscape)

@[inline]

def Lean.isIdEndEscape (c : Char) : Bool

Equations

• Lean.isIdEndEscape c = decide (c = Lean.idEndEscape)

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

Equations

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

@[export lean_is_inaccessible_user_name]

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

Equations

• (pre.str s).isInaccessibleUserName = (s.contains '✝' || s == "_inaccessible")
• (p.num i).isInaccessibleUserName = p.isInaccessibleUserName
• x✝.isInaccessibleUserName = false

def Lean.Name.escapePart (s : String) (force : Bool := false) : Option String

Creates a round-trippable string name component if possible, otherwise returns none. Names that are valid identifiers are not escaped, and otherwise, if they do not contain », they are escaped.

• If force is true, then even valid identifiers are escaped.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Name.toStringWithSep (sep : String) (escape : Bool) (n : Lean.Name) (isToken : String → Bool := fun (x : String) => false) : String

Uses the separator sep (usually ".") to combine the components of the Name into a string. See the documentation for Name.toString for an explanation of escape and isToken.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Name.toStringWithSep sep escape Lean.Name.anonymous isToken = "[anonymous]"
• Lean.Name.toStringWithSep sep escape (Lean.Name.anonymous.str s) isToken = Lean.Name.toStringWithSep.maybeEscape escape s (isToken s)
• Lean.Name.toStringWithSep sep escape (Lean.Name.anonymous.num v) isToken = toString v
• Lean.Name.toStringWithSep sep escape (n_2.num v) isToken = Lean.Name.toStringWithSep sep escape n_2 ++ sep ++ v.repr

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

Equations

• Lean.Name.toStringWithSep.maybeEscape escape s force = if escape = true then (Lean.Name.escapePart s force).getD s else s

def Lean.Name.toString (n : Lean.Name) (escape : Bool := true) (isToken : String → Bool := fun (x : String) => false) : String

Converts a name to a string.

• If escape is true, then escapes name components using « and » to ensure that those names that can appear in source files round trip. Names with number components, anonymous names, and names containing » might not round trip. Furthermore, "pseudo-syntax" produced by the delaborator, such as _, #0 or ?u, is not escaped.
• The optional isToken function is used when escape is true to determine whether more escaping is necessary to avoid parser tokens. The insertion algorithm works so long as parser tokens do not themselves contain « or ».

Equations

• n.toString escape isToken = Lean.Name.toStringWithSep "." (escape && !n.isInaccessibleUserName && !n.hasMacroScopes && !Lean.Name.toString.maybePseudoSyntax n) n isToken

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

Equations

• Lean.Name.toString.maybePseudoSyntax n = if (n == `_) = true then true else match n.getRoot with | pre.str s => "#".isPrefixOf s || "?".isPrefixOf s | x => false

instance Lean.Name.instToString : ToString Lean.Name

Equations

• Lean.Name.instToString = { toString := fun (n : Lean.Name) => n.toString }

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

Equations

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

instance Lean.Name.instRepr : Repr Lean.Name

Equations

• Lean.Name.instRepr = { reprPrec := Lean.Name.reprPrec }

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

Equations

• (pre.str s).capitalize = pre.str s.capitalize
• x✝.capitalize = x✝

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

Equations

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

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

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

Equations

• x✝.eraseSuffix? Lean.Name.anonymous = some x✝
• (p.str s).eraseSuffix? (p'.str s') = if (s == s') = true then p.eraseSuffix? p' else none
• (p.num s).eraseSuffix? (p'.num s') = if (s == s') = true then p.eraseSuffix? p' else none
• x✝¹.eraseSuffix? x✝ = none

@[inline]

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

Remove macros scopes, apply f, and put them back

Equations

• One or more equations did not get rendered due to their size.

@[export lean_name_append_after]

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

Equations

• n.appendAfter suffix = n.modifyBase fun (x : Lean.Name) => match x with | p.str s => p.mkStr (s ++ suffix) | n => n.mkStr suffix

@[export lean_name_append_index_after]

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

Equations

• n.appendIndexAfter idx = n.modifyBase fun (x : Lean.Name) => match x with | p.str s => p.mkStr (s ++ "_" ++ toString idx) | n => n.mkStr ("_" ++ toString idx)

@[export lean_name_append_before]

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

Equations

• One or more equations did not get rendered due to their size.

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

instance Lean.Name.instLawfulBEq : LawfulBEq Lean.Name

instance Lean.Name.instDecidableEq : DecidableEq Lean.Name

Equations

• a.instDecidableEq b = if h : (a == b) = true then isTrue ⋯ else isFalse ⋯

@[inline]

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

Equations

• g.curr = g.namePrefix.mkNum g.idx

@[inline]

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

Equations

• g.next = { namePrefix := g.namePrefix, idx := g.idx + 1 }

@[inline]

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

Equations

• g.mkChild = ({ namePrefix := g.namePrefix.mkNum g.idx, idx := 1 }, { namePrefix := g.namePrefix, idx := g.idx + 1 })

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 Lean.Name

Equations

• Lean.mkFreshId = do let ngen ← Lean.getNGen let r : Lean.Name := ngen.curr Lean.setNGen ngen.next pure r

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

Equations

• Lean.monadNameGeneratorLift m n = { getNGen := liftM Lean.getNGen, setNGen := fun (ngen : Lean.NameGenerator) => liftM (Lean.setNGen ngen) }

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

Equations

• Lean.Syntax.instReprPreresolved = { reprPrec := Lean.Syntax.reprPreresolved✝ }

instance Lean.Syntax.instRepr : Repr Lean.Syntax

Equations

• Lean.Syntax.instRepr = { reprPrec := Lean.Syntax.reprSyntax✝ }

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

Equations

• Lean.Syntax.instReprTSyntax = { reprPrec := Lean.Syntax.reprTSyntax✝ }

@[reducible, inline]

abbrev Lean.Syntax.Term : Type

Equations

• Lean.Term = Lean.TSyntax `term

@[reducible, inline]

abbrev Lean.Syntax.Command : Type

Equations

• Lean.Command = Lean.TSyntax `command

@[reducible, inline]

abbrev Lean.Syntax.Level : Type

Equations

• Lean.Syntax.Level = Lean.TSyntax `level

@[reducible, inline]

abbrev Lean.Syntax.Tactic : Type

Equations

• Lean.Syntax.Tactic = Lean.TSyntax `tactic

@[reducible, inline]

abbrev Lean.Syntax.Prec : Type

Equations

• Lean.Prec = Lean.TSyntax `prec

@[reducible, inline]

abbrev Lean.Syntax.Prio : Type

Equations

• Lean.Prio = Lean.TSyntax `prio

@[reducible, inline]

abbrev Lean.Syntax.Ident : Type

Equations

• Lean.Ident = Lean.TSyntax Lean.identKind

@[reducible, inline]

abbrev Lean.Syntax.StrLit : Type

Equations

• Lean.StrLit = Lean.TSyntax Lean.strLitKind

@[reducible, inline]

abbrev Lean.Syntax.CharLit : Type

Equations

• Lean.CharLit = Lean.TSyntax Lean.charLitKind

@[reducible, inline]

abbrev Lean.Syntax.NameLit : Type

Equations

• Lean.NameLit = Lean.TSyntax Lean.nameLitKind

@[reducible, inline]

abbrev Lean.Syntax.ScientificLit : Type

Equations

• Lean.ScientificLit = Lean.TSyntax Lean.scientificLitKind

@[reducible, inline]

abbrev Lean.Syntax.NumLit : Type

Equations

• Lean.NumLit = Lean.TSyntax Lean.numLitKind

@[reducible, inline]

abbrev Lean.Syntax.HygieneInfo : Type

Equations

• Lean.HygieneInfo = Lean.TSyntax Lean.hygieneInfoKind

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

Equations

• Lean.TSyntax.instCoeConsSyntaxNodeKindNil = { coe := fun (stx : Lean.TSyntax k) => { raw := stx.raw } }

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

Equations

• Lean.TSyntax.instCoeConsSyntaxNodeKind = { coe := fun (stx : Lean.TSyntax ks) => { raw := stx.raw } }

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

Equations

• Lean.TSyntax.instCoeIdentTerm = { coe := fun (s : Lean.Ident) => { raw := s.raw } }

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

Equations

• Lean.TSyntax.instCoeDepTermMkIdentIdent = { coe := { raw := Lean.Syntax.ident info ss n res } }

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

Equations

• Lean.TSyntax.instCoeStrLitTerm = { coe := fun (s : Lean.StrLit) => { raw := s.raw } }

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

Equations

• Lean.TSyntax.instCoeNameLitTerm = { coe := fun (s : Lean.NameLit) => { raw := s.raw } }

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

Equations

• Lean.TSyntax.instCoeScientificLitTerm = { coe := fun (s : Lean.ScientificLit) => { raw := s.raw } }

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

Equations

• Lean.TSyntax.instCoeNumLitTerm = { coe := fun (s : Lean.NumLit) => { raw := s.raw } }

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

Equations

• Lean.TSyntax.instCoeCharLitTerm = { coe := fun (s : Lean.CharLit) => { raw := s.raw } }

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

Equations

• Lean.TSyntax.instCoeIdentLevel = { coe := fun (s : Lean.Ident) => { raw := s.raw } }

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

Equations

• Lean.TSyntax.instCoeNumLitPrio = { coe := fun (s : Lean.NumLit) => { raw := s.raw } }

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

Equations

• Lean.TSyntax.instCoeNumLitPrec = { coe := fun (s : Lean.NumLit) => { raw := s.raw } }

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

Equations

• Lean.TSyntax.Compat.instCoeTailSyntax = { coe := fun (s : Lean.Syntax) => { raw := s } }

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

Equations

• Lean.TSyntax.Compat.instCoeTailArraySyntaxTSyntaxArray = { coe := Lean.TSyntaxArray.mk }

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

Equations

• Lean.Syntax.instBEqPreresolved = { beq := Lean.Syntax.beqPreresolved✝ }

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

Compare syntax structures modulo source info.

instance Lean.Syntax.instBEq : BEq Lean.Syntax

Equations

• Lean.Syntax.instBEq = { beq := Lean.Syntax.structEq }

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

Equations

• Lean.Syntax.instBEqTSyntax = { beq := fun (x1 x2 : Lean.TSyntax k) => x1.raw == x2.raw }

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

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

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

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

Equations

• stx.getTailInfo = stx.getTailInfo?.getD Lean.SourceInfo.none

def Lean.Syntax.getTrailingSize (stx : Lean.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.

Equations

• stx.getTrailingSize = match stx.getTailInfo? with | some (Lean.SourceInfo.original leading pos trailing endPos) => trailing.bsize | x => 0

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

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.

Equations

• stx.getTrailing? = stx.getTailInfo.getTrailing?

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

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.

Equations

• stx.getTrailingTailPos? canonicalOnly = stx.getTailInfo.getTrailingTailPos? canonicalOnly

def Lean.Syntax.getSubstring? (stx : Lean.Syntax) (withLeading withTrailing : 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).

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• stx.setTailInfo info = match Lean.Syntax.setTailInfoAux info stx with | some stx => stx | none => stx

def Lean.Syntax.unsetTrailing (stx : Lean.Syntax) : Lean.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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• stx.setHeadInfo info = match Lean.Syntax.setHeadInfoAux info stx with | some stx => stx | none => stx

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

Equations

• Lean.Syntax.setInfo info (Lean.Syntax.atom info_1 val) = Lean.Syntax.atom info val
• Lean.Syntax.setInfo info (Lean.Syntax.ident info_1 rawVal val pre) = Lean.Syntax.ident info rawVal val pre
• Lean.Syntax.setInfo info (Lean.Syntax.node info_1 kind args) = Lean.Syntax.node info kind args
• Lean.Syntax.setInfo info Lean.Syntax.missing = Lean.Syntax.missing

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

Return the first atom/identifier that has position information

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

Equations

• target.copyHeadTailInfoFrom source = (target.setHeadInfo source.getHeadInfo).setTailInfo source.getTailInfo

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.

Equations

• stx.mkSynthetic = stx.setHeadInfo (Lean.SourceInfo.fromRef stx)

@[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

Equations

• Lean.withHeadRefOnly x = do let __do_lift ← Lean.getRef match __do_lift.getHead? with | none => x | some ref => Lean.withRef ref x

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

Helper functions for processing Syntax programmatically

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

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

Equations

• Lean.mkIdentFrom src val canonical = { raw := Lean.Syntax.ident (Lean.SourceInfo.fromRef src canonical) (toString val).toSubstring val [] }

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

Equations

• Lean.mkIdentFromRef val canonical = do let __do_lift ← Lean.getRef pure (Lean.mkIdentFrom __do_lift val canonical)

def Lean.mkCIdentFrom (src : Lean.Syntax) (c : Lean.Name) (canonical : 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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.mkCIdentFromRef c canonical = do let __do_lift ← Lean.getRef pure (Lean.mkCIdentFrom __do_lift c canonical).raw

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

Equations

• Lean.mkCIdent c = Lean.mkCIdentFrom Lean.Syntax.missing c

@[export lean_mk_syntax_ident]

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

Equations

• Lean.mkIdent val = { raw := Lean.Syntax.ident Lean.SourceInfo.none (toString val).toSubstring val [] }

@[inline]

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

Equations

• Lean.mkGroupNode args = (Lean.mkNode Lean.groupKind args).raw

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.mkOptionalNode (some stx) = Lean.mkNullNode #[stx]
• Lean.mkOptionalNode none = Lean.mkNullNode #[]

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

Equations

• Lean.mkHole ref canonical = (Lean.mkNode `Lean.Parser.Term.hole #[Lean.mkAtomFrom ref "_" canonical]).raw

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

Equations

• Lean.Syntax.mkSep a sep = Lean.mkNullNode (Lean.mkSepArray a sep)

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

Equations

• Lean.Syntax.SepArray.ofElems elems = { elemsAndSeps := Lean.mkSepArray elems (if sep.isEmpty = true then Lean.mkNullNode else Lean.mkAtom 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)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Syntax.instCoeArraySepArray = { coe := Lean.Syntax.SepArray.ofElems }

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

Constructs a typed separated array from elements. The given array does not include the separators.

Like Syntax.SepArray.ofElems but for typed syntax.

Equations

• Lean.Syntax.TSepArray.ofElems elems = { elemsAndSeps := (Lean.Syntax.SepArray.ofElems (Lean.TSyntaxArray.raw elems)).elemsAndSeps }

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

Equations

• Lean.Syntax.instCoeTSyntaxArrayTSepArray = { coe := Lean.Syntax.TSepArray.ofElems }

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.

Equations

• Lean.Syntax.mkApp fn x✝ = match x✝ with | #[] => fn | args => { raw := (Lean.mkNode `Lean.Parser.Term.app #[fn.raw, Lean.mkNullNode args.raw]).raw }

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

Equations

• Lean.Syntax.mkCApp fn args = Lean.Syntax.mkApp { raw := (Lean.mkCIdent fn).raw } args

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

Equations

• Lean.Syntax.mkLit kind val info = Lean.mkNode kind #[Lean.Syntax.atom info val]

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

Equations

• Lean.Syntax.mkCharLit val info = Lean.Syntax.mkLit Lean.charLitKind val.quote info

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

Equations

• Lean.Syntax.mkStrLit val info = Lean.Syntax.mkLit Lean.strLitKind val.quote info

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

Equations

• Lean.Syntax.mkNumLit val info = Lean.Syntax.mkLit Lean.numLitKind val info

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

Equations

• Lean.Syntax.mkNatLit val info = Lean.Syntax.mkLit Lean.numLitKind (toString val) info

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

Equations

• Lean.Syntax.mkScientificLit val info = Lean.Syntax.mkLit Lean.scientificLitKind val info

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

Equations

• Lean.Syntax.mkNameLit val info = Lean.Syntax.mkLit Lean.nameLitKind val info

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Syntax.isLit? litKind stx = none

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

Equations

• s.isNatLit? = Lean.Syntax.isNatLitAux✝ Lean.numLitKind s

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

Equations

• s.isFieldIdx? = Lean.Syntax.isNatLitAux✝ Lean.fieldIdxKind s

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.

Equations

• Lean.Syntax.decodeScientificLitVal? s = if (s.length == 0) = true then none else let c := s.get 0; if c.isDigit = true then Lean.Syntax.decodeScientificLitVal?.decode s 0 0 else none

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

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

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Syntax.decodeScientificLitVal?.decodeAfterDot (s : String) (i : String.Pos) (val 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)

Equations

• stx.isScientificLit? = match Lean.Syntax.isLit? Lean.scientificLitKind stx with | some val => Lean.Syntax.decodeScientificLitVal? val | x => none

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

Equations

• (Lean.Syntax.atom info val).isIdOrAtom? = some val
• (Lean.Syntax.ident info rawVal val preresolved).isIdOrAtom? = some rawVal.toString
• x✝.isIdOrAtom? = none

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

Equations

• stx.toNat = match stx.isNatLit? with | some val => val | none => 0

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

Equations

• One or more equations did not get rendered due to their size.

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

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 \.

Equations

• Lean.Syntax.decodeStringGap s i = do guard ((s.get i).isWhitespace = true) some (s.nextWhile Char.isWhitespace (s.next i))

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

partial def Lean.Syntax.decodeRawStrLitAux (s : String) (i : String.Pos) (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.

Equations

• Lean.Syntax.decodeStrLit s = if (s.get 0 == 'r') = true then some (Lean.Syntax.decodeRawStrLitAux s { byteIdx := 1 } 0) else Lean.Syntax.decodeStrLitAux s { byteIdx := 1 } ""

def Lean.Syntax.isStrLit? (stx : Lean.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.

Equations

• stx.isStrLit? = match Lean.Syntax.isLit? Lean.strLitKind stx with | some val => Lean.Syntax.decodeStrLit val | x => none

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• stx.isCharLit? = match Lean.Syntax.isLit? Lean.charLitKind stx with | some val => Lean.Syntax.decodeCharLit val | x => none

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 [].

Equations

• Lean.Syntax.splitNameLit ss = (Lean.Syntax.splitNameLitAux✝ ss []).reverse

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

Equations

• One or more equations did not get rendered due to their size.

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

Converts a String to a hierarchical Name after splitting it at the dots.

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

Equations

• s.toName = s.toSubstring.toName

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

Equations

• Lean.Syntax.decodeNameLit s = if (s.get 0 == '`') = true then match (s.toSubstring.drop 1).toName with | Lean.Name.anonymous => none | name => some name else none

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

Equations

• stx.isNameLit? = match Lean.Syntax.isLit? Lean.nameLitKind stx with | some val => Lean.Syntax.decodeNameLit val | x => none

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

Equations

• (Lean.Syntax.node info k args).hasArgs = decide (args.size > 0)
• x✝.hasArgs = false

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

Equations

• (Lean.Syntax.atom info val).isAtom = true
• x✝.isAtom = false

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

Equations

• Lean.Syntax.isToken token (Lean.Syntax.atom info val) = (val.trim == token.trim)
• Lean.Syntax.isToken token x✝ = false

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

Equations

• (Lean.Syntax.node info k args).isNone = (k == Lean.nullKind && args.size == 0)
• Lean.Syntax.missing.isNone = true
• stx.isNone = false

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

Equations

• stx.getOptionalIdent? = match stx.getOptional? with | some stx => some stx.getId | none => none

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

Equations

• stx.find? p = Lean.Syntax.findAux p stx

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

Equations

• Lean.TSyntax.getNat s = s.raw.isNatLit?.getD 0

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

Equations

• Lean.TSyntax.getId s = s.raw.getId

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

Equations

• Lean.TSyntax.getScientific s = s.raw.isScientificLit?.getD (0, false, 0)

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

Equations

• Lean.TSyntax.getString s = s.raw.isStrLit?.getD ""

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

Equations

• Lean.TSyntax.getChar s = s.raw.isCharLit?.getD default

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

Equations

• Lean.TSyntax.getName s = s.raw.isNameLit?.getD Lean.Name.anonymous

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

Equations

• Lean.TSyntax.getHygieneInfo s = s.raw[0].getId

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

Equations

• Lean.TSyntax.Compat.instCoeTailArraySyntaxTSepArray = { coe := fun (a : Array Lean.Syntax) => Lean.Syntax.TSepArray.ofElems (Lean.TSyntaxArray.mk a) }

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

Equations

• One or more equations did not get rendered due to their size.

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

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

• quote : α → Lean.TSyntax k

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

Equations

• Lean.instQuoteOfCoeHTCTTSyntaxConsSyntaxNodeKindNil = { quote := fun (a : α) => CoeHTCT.coe (Lean.quote a) }

instance Lean.instQuoteTermMkStr1 : Lean.Quote Lean.Term

Equations

• Lean.instQuoteTermMkStr1 = Lean.Quote.mk `term id

instance Lean.instQuoteBoolMkStr1 : Lean.Quote Bool

Equations

• Lean.instQuoteBoolMkStr1 = Lean.Quote.mk `term fun (x : Bool) => match x with | true => { raw := (Lean.mkCIdent `Bool.true).raw } | false => { raw := (Lean.mkCIdent `Bool.false).raw }

instance Lean.instQuoteCharCharLitKind : Lean.Quote Char Lean.charLitKind

Equations

• Lean.instQuoteCharCharLitKind = { quote := fun (val : Char) => Lean.Syntax.mkCharLit val }

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

Equations

• Lean.instQuoteStringStrLitKind = { quote := fun (val : String) => Lean.Syntax.mkStrLit val }

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

Equations

• Lean.instQuoteNatNumLitKind = { quote := fun (n : Nat) => Lean.Syntax.mkNumLit (toString n) }

instance Lean.instQuoteSubstringMkStr1 : Lean.Quote Substring

Equations

• Lean.instQuoteSubstringMkStr1 = Lean.Quote.mk `term fun (s : Substring) => Lean.Syntax.mkCApp `String.toSubstring' #[Lean.quote `term s.toString]

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

Equations

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

instance Lean.instQuoteNameMkStr1 : Lean.Quote Lean.Name

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.instQuoteProdMkStr1 = Lean.Quote.mk `term fun (x : α × β) => match x with | (a, b) => Lean.Syntax.mkCApp `Prod.mk #[Lean.quote `term a, Lean.quote `term b]

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

Equations

• Lean.instQuoteListMkStr1 = Lean.Quote.mk `term Lean.quoteList✝

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

Equations

• Lean.instQuoteArrayMkStr1 = Lean.Quote.mk `term Lean.quoteArray✝

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

Equations

• One or more equations did not get rendered due to their size.

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

Evaluator for prec DSL

Equations

• One or more equations did not get rendered due to their size.

def Lean.termEval_prec_ : Lean.ParserDescr

Equations

• Lean.termEval_prec_ = Lean.ParserDescr.node `Lean.termEval_prec_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "eval_prec ") (Lean.ParserDescr.cat `prec 1024))

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

Evaluator for prio DSL

Equations

• One or more equations did not get rendered due to their size.

def Lean.termEval_prio_ : Lean.ParserDescr

Equations

• Lean.termEval_prio_ = Lean.ParserDescr.node `Lean.termEval_prio_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "eval_prio ") (Lean.ParserDescr.cat `prio 1024))

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

Equations

• Lean.evalOptPrio (some prio) = Lean.evalPrio prio.raw
• Lean.evalOptPrio none = pure 1000

@[reducible, inline]

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

Equations

• @Array.getSepElems = @Array.getEvenElems

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

Equations

• a.filterSepElemsM p = Array.filterSepElemsMAux✝ a p 0 #[]

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

Equations

• a.filterSepElems p = (a.filterSepElemsM p).run

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

Equations

• a.mapSepElemsM f = Array.mapSepElemsMAux✝ a f 0 #[]

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

Equations

• a.mapSepElems f = (a.mapSepElemsM f).run

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

Equations

• sa.getElems = sa.elemsAndSeps.getSepElems

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

Equations

• sa.getElems = Lean.TSyntaxArray.mk sa.elemsAndSeps.getSepElems

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

Equations

• sa.push e = if sa.elemsAndSeps.isEmpty = true then { elemsAndSeps := #[e.raw] } else { elemsAndSeps := (sa.elemsAndSeps.push (Lean.mkAtom sep)).push e.raw }

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

Equations

• Lean.Syntax.instEmptyCollectionSepArray = { emptyCollection := { elemsAndSeps := ∅ } }

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

Equations

• Lean.Syntax.instEmptyCollectionTSepArray = { emptyCollection := { elemsAndSeps := ∅ } }

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

Equations

• Lean.Syntax.instCoeOutSepArrayArray = { coe := Lean.Syntax.SepArray.getElems }

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

Equations

• Lean.Syntax.instCoeOutTSepArrayTSyntaxArray = { coe := Lean.Syntax.TSepArray.getElems }

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

Equations

• Lean.Syntax.instCoeTSyntaxArrayOfTSyntax = { coe := fun (a : Lean.TSyntaxArray k) => Array.map Coe.coe a }

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

Equations

• Lean.Syntax.instCoeOutTSyntaxArrayArray = { coe := fun (a : Lean.TSyntaxArray k) => a.raw }

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

Equations

• Lean.Syntax.instCoeIdentTSyntaxConsSyntaxNodeKindMkStr4Nil = { coe := fun (id : Lean.Ident) => Lean.mkNode `Lean.Parser.Command.declId #[id.raw, Lean.mkNullNode #[]] }

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

Equations

• Lean.Syntax.instCoeTermTSyntaxConsSyntaxNodeKindMkStr4Nil = { coe := fun (stx : Lean.Term) => { raw := stx.raw } }

Helper functions for manipulating interpolated strings

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

Equations

• stx.isInterpolatedStrLit? = match Lean.Syntax.isLit? Lean.interpolatedStrLitKind stx with | none => none | some val => Lean.Syntax.decodeInterpStrLit✝ val

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

Equations

• stx.getSepArgs = stx.getArgs.getSepElems

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• stx.getDocString = match stx.raw[1] with | Lean.Syntax.atom info val => val.extract 0 (val.endPos - { byteIdx := 2 }) | x => ""

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

Equations

• Lean.Meta.instReprConfig_1 = { reprPrec := Lean.Meta.reprConfig✝ }

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

Equations

• Lean.Meta.instReprConfig = { reprPrec := Lean.Meta.reprConfig✝ }

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

Equations

• Lean.Meta.instReprEtaStructMode = { reprPrec := Lean.Meta.reprEtaStructMode✝ }

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

Equations

• Lean.Meta.instReprTransparencyMode = { reprPrec := Lean.Meta.reprTransparencyMode✝ }

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

Equations

• Lean.Meta.Occurrences.all.contains x✝ = true
• (Lean.Meta.Occurrences.pos idxs).contains x✝ = idxs.contains x✝
• (Lean.Meta.Occurrences.neg idxs).contains x✝ = !idxs.contains x✝

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

Equations

• Lean.Meta.Occurrences.all.isAll = true
• x✝.isAll = false

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 : Lean.Meta.ApplyNewGoals
• nonDependentOnly : Lean.Meta.ApplyNewGoals
• all : Lean.Meta.ApplyNewGoals

structure Lean.Meta.ApplyConfig : Type

Configures the behaviour of the apply tactic.

• newGoals : Lean.Meta.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

Equations

• Lean.Meta.Rewrite.NewGoals = Lean.Meta.ApplyNewGoals

structure Lean.Meta.Rewrite.Config : Type

• transparency : Lean.Meta.TransparencyMode
• offsetCnstrs : Bool
• occs : Lean.Meta.Occurrences
• newGoals : Lean.Meta.Rewrite.NewGoals

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 : α) : Lean.Meta.CheckTactic.CheckGoalType val

partial def Lean.Parser.Tactic.getConfigItems (c : Lean.Syntax) : Lean.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 : Lean.TSyntaxArray `Lean.Parser.Tactic.configItem) : Lean.TSyntax `Lean.Parser.Tactic.optConfig

Equations

• Lean.Parser.Tactic.mkOptConfig items = { raw := Lean.Syntax.node1 Lean.SourceInfo.none `Lean.Parser.Tactic.optConfig (Lean.mkNullNode items.raw) }

def Lean.Parser.Tactic.appendConfig (cfg cfg' : Lean.Syntax) : Lean.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)?).

Equations

• Lean.Parser.Tactic.appendConfig cfg cfg' = Lean.Parser.Tactic.mkOptConfig (Lean.Parser.Tactic.getConfigItems cfg ++ Lean.Parser.Tactic.getConfigItems cfg')

def Lean.Parser.Tactic.tacticErw___ : Lean.ParserDescr

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

simp_all_arith combines the effects of simp_all and simp_arith.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.