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

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.

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))

def Lean.isIdFirst (c : Char) : Bool

Equations

• Lean.isIdFirst c = (Char.isAlpha c || decide (c = Char.ofNat 95) || Lean.isLetterLike c)

def Lean.isIdRest (c : Char) : Bool

Equations

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

def Lean.idBeginEscape : Char

Equations

• Lean.idBeginEscape = Char.ofNat 171

def Lean.idEndEscape : Char

Equations

• Lean.idEndEscape = Char.ofNat 187

def Lean.isIdBeginEscape (c : Char) : Bool

Equations

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

def Lean.isIdEndEscape (c : Char) : Bool

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Name.toString.maybePseudoSyntax n = match Lean.Name.getRoot n with | Lean.Name.str pre s => String.isPrefixOf "#" s || String.isPrefixOf "?" s | x => false

instance Lean.Name.instToStringName : ToString Lake.Name

Equations

• Lean.Name.instToStringName = { toString := fun n => Lean.Name.toString n }

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

Equations

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

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

Equations

• Lean.Name.capitalize x = match x with | Lean.Name.str p s => Lean.Name.str p (String.capitalize s) | n => n

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

Equations

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

@[export lean_name_append_after]

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

Equations

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

@[export lean_name_append_index_after]

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

Equations

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

@[export lean_name_append_before]

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

Equations

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

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

instance Lean.Name.instLawfulBEqNameInstBEqName : LawfulBEq Lake.Name

Equations

• Lean.Name.instLawfulBEqNameInstBEqName = Lean.Name.instLawfulBEqNameInstBEqName.proof_1

instance Lean.Name.instDecidableEqName : DecidableEq Lake.Name

Equations

• Lean.Name.instDecidableEqName a b = if h : (a == b) = true then isTrue (_ : a = b) else isFalse (_ : ¬a = b)

structure Lean.NameGenerator : Type

• namePrefix : Lake.Name
• idx : Nat

instance Lean.instInhabitedNameGenerator : Inhabited Lean.NameGenerator

Equations

• Lean.instInhabitedNameGenerator = { default := { namePrefix := default, idx := default } }

@[inline]

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

Equations

• Lean.NameGenerator.curr g = Lean.Name.mkNum g.namePrefix g.idx

@[inline]

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

Equations

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

@[inline]

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

Equations

• Lean.NameGenerator.mkChild g = ({ namePrefix := Lean.Name.mkNum g.namePrefix 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 Lake.Name

Equations

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

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

Equations

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

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

Equations

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

instance Lean.Syntax.instReprSyntax : Repr Lean.Syntax

Equations

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

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

Equations

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

@[inline, reducible]

abbrev Lean.Syntax.Term : Type

Equations

• Lean.Term = Lean.TSyntax `term

@[inline, reducible]

abbrev Lean.Syntax.Command : Type

Equations

• Lean.Command = Lean.TSyntax `command

@[inline, reducible]

abbrev Lean.Syntax.Level : Type

Equations

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

@[inline, reducible]

abbrev Lean.Syntax.Tactic : Type

Equations

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

@[inline, reducible]

abbrev Lean.Syntax.Prec : Type

Equations

• Lean.Prec = Lean.TSyntax `prec

@[inline, reducible]

abbrev Lean.Syntax.Prio : Type

Equations

• Lean.Prio = Lean.TSyntax `prio

@[inline, reducible]

abbrev Lean.Syntax.Ident : Type

Equations

• Lean.Ident = Lean.TSyntax Lean.identKind

@[inline, reducible]

abbrev Lean.Syntax.StrLit : Type

Equations

• Lean.StrLit = Lean.TSyntax Lean.strLitKind

@[inline, reducible]

abbrev Lean.Syntax.CharLit : Type

Equations

• Lean.CharLit = Lean.TSyntax Lean.charLitKind

@[inline, reducible]

abbrev Lean.Syntax.NameLit : Type

Equations

• Lean.NameLit = Lean.TSyntax Lean.nameLitKind

@[inline, reducible]

abbrev Lean.Syntax.ScientificLit : Type

Equations

• Lean.ScientificLit = Lean.TSyntax Lean.scientificLitKind

@[inline, reducible]

abbrev Lean.Syntax.NumLit : Type

Equations

• Lean.NumLit = Lean.TSyntax Lean.numLitKind

@[inline, reducible]

abbrev Lean.Syntax.HygieneInfo : Type

Equations

• Lean.HygieneInfo = Lean.TSyntax Lean.hygieneInfoKind

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

Equations

• Lean.TSyntax.instCoeTSyntaxConsSyntaxNodeKindNil = { coe := fun stx => { raw := stx.raw } }

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

Equations

• Lean.TSyntax.instCoeTSyntaxConsSyntaxNodeKind = { coe := fun stx => { raw := stx.raw } }

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

Equations

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

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

Equations

• Lean.TSyntax.instCoeDepTermMkConsSyntaxNodeKindMkStr1NilIdentIdent = { 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 => { raw := s.raw } }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.TSyntax.Compat.instCoeTailSyntaxTSyntax = { coe := fun s => { 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.instBEqSyntax : BEq Lean.Syntax

Equations

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

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

Equations

• Lean.Syntax.instBEqTSyntax = { beq := fun x x_1 => x.raw == x_1.raw }

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

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

Equations

• Lean.Syntax.getTailInfo stx = Option.getD (Lean.Syntax.getTailInfo? stx) Lean.SourceInfo.none

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

Equations

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

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

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

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

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

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

• Lean.Syntax.setHeadInfo stx 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

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

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

Equations

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

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

• Lean.Syntax.mkSynthetic stx = Lean.Syntax.setHeadInfo stx (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 Lean.Syntax.getHead? __do_lift with | none => x | some ref => Lean.withRef ref x

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.

Equations

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

def Lean.mkIdentFromRef {m : Type → Type} [Monad m] [Lean.MonadRef m] (val : Lake.Name) (canonical : optParam 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 : 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.

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 : Lake.Name) (canonical : optParam 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 : Lake.Name) : Lean.Ident

Equations

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

@[export lean_mk_syntax_ident]

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

Equations

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

@[inline]

def Lean.mkGroupNode (args : optParam (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 arg = match arg with | some arg => Lean.mkNullNode #[arg] | none => Lean.mkNullNode #[]

def Lean.mkHole (ref : Lean.Syntax) (canonical : optParam 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 String.isEmpty sep = 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.instCoeArraySyntaxSepArray {sep : String} : Coe (Array Lean.Syntax) (Lean.Syntax.SepArray sep)

Equations

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

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

Equations

• Lean.Syntax.instCoeTSyntaxArrayTSepArray = { coe := fun a => { elemsAndSeps := Lean.mkSepArray (Lean.TSyntaxArray.raw a) (Lean.mkAtom 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.

Equations

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

def Lean.Syntax.mkCApp (fn : Lake.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 : optParam Lean.SourceInfo Lean.SourceInfo.none) : Lean.TSyntax kind

Equations

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

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

Equations

• Lean.Syntax.mkStrLit val info = Lean.Syntax.mkLit Lean.strLitKind (String.quote val) info

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

Equations

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

def Lean.Syntax.mkScientificLit (val : String) (info : optParam 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 : optParam 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.

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

Equations

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

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

Equations

• Lean.Syntax.isFieldIdx? s = 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

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

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)

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 : 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)

Equations

• Lean.Syntax.isScientificLit? stx = 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.isIdOrAtom? x = match x with | Lean.Syntax.atom info val => some val | Lean.Syntax.ident info rawVal val preresolved => some (Substring.toString rawVal) | x => none

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

Equations

• Lean.Syntax.toNat stx = match Lean.Syntax.isNatLit? stx 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.

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

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

Equations

• Lean.Syntax.decodeStrLit s = Lean.Syntax.decodeStrLitAux s { byteIdx := 1 } ""

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

Equations

• Lean.Syntax.isStrLit? stx = 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

• Lean.Syntax.isCharLit? stx = 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 = List.reverse (Lean.Syntax.splitNameLitAux ss [])

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

Equations

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

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

Equations

• String.toName s = Substring.toName (String.toSubstring s)

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

Equations

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

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

Equations

• Lean.Syntax.isNameLit? stx = 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.hasArgs x = match x with | Lean.Syntax.node info kind args => decide (Array.size args > 0) | x => false

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

Equations

• Lean.Syntax.isAtom x = match x with | Lean.Syntax.atom info val => true | x => false

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

Equations

• Lean.Syntax.isToken token x = match x with | Lean.Syntax.atom info val => String.trim val == String.trim token | x => false

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

Equations

• Lean.Syntax.isNone stx = match stx with | Lean.Syntax.node info k args => k == Lean.nullKind && Array.size args == 0 | Lean.Syntax.missing => true | x => false

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

Equations

• Lean.Syntax.getOptionalIdent? stx = match Lean.Syntax.getOptional? stx with | some stx => some (Lean.Syntax.getId stx) | 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

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

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

Equations

• Lean.TSyntax.getNat s = Option.getD (Lean.Syntax.isNatLit? s.raw) 0

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

Equations

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

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

Equations

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

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

Equations

• Lean.TSyntax.getString s = Option.getD (Lean.Syntax.isStrLit? s.raw) ""

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

Equations

• Lean.TSyntax.getChar s = Option.getD (Lean.Syntax.isCharLit? s.raw) default

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

Equations

• Lean.TSyntax.getName s = Option.getD (Lean.Syntax.isNameLit? s.raw) Lean.Name.anonymous

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

Equations

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

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 => { elemsAndSeps := Lean.mkSepArray (Lean.TSyntaxArray.raw (Lean.TSyntaxArray.mk a)) (Lean.mkAtom sep) } }

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

Equations

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

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'

Equations

• Lean.instQuote = Lean.Quote.mk k' fun a => CoeHTCT.coe (Lean.quote k 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 => match x with | true => { raw := (Lean.mkCIdent `Bool.true).raw } | false => { raw := (Lean.mkCIdent `Bool.false).raw }

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

Equations

• Lean.instQuoteStringStrLitKind = Lean.Quote.mk Lean.strLitKind fun val => Lean.Syntax.mkStrLit val

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

Equations

• Lean.instQuoteNatNumLitKind = Lean.Quote.mk Lean.numLitKind fun n => Lean.Syntax.mkNumLit (toString n)

instance Lean.instQuoteSubstringMkStr1 : Lean.Quote Substring

Equations

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

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

Equations

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

instance Lean.instQuoteProdMkStr1 {α : Type} {β : 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 x = match x with | some prio => Lean.evalPrio prio.raw | none => pure 1000

@[inline, reducible]

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Syntax.SepArray.getElems sa = Array.getSepElems sa.elemsAndSeps

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

Equations

• Lean.Syntax.TSepArray.getElems sa = Lean.TSyntaxArray.mk (Array.getSepElems sa.elemsAndSeps)

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

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

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.instCoeOutSepArrayArraySyntax {sep : String} : CoeOut (Lean.Syntax.SepArray sep) (Array Lean.Syntax)

Equations

• Lean.Syntax.instCoeOutSepArrayArraySyntax = { 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.instCoeTSyntaxArray {k : Lean.SyntaxNodeKinds} {k' : Lean.SyntaxNodeKinds} [Coe (Lean.TSyntax k) (Lean.TSyntax k')] : Coe (Lean.TSyntaxArray k) (Lean.TSyntaxArray k')

Equations

• Lean.Syntax.instCoeTSyntaxArray = { coe := fun a => Array.map Coe.coe a }

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

Equations

• Lean.Syntax.instCoeOutTSyntaxArrayArraySyntax = { coe := fun a => Lean.TSyntaxArray.raw a }

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

Equations

• Lean.Syntax.instCoeIdentTSyntaxConsSyntaxNodeKindMkStr4Nil = { coe := fun id => 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 => { raw := stx.raw } }

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

Equations

• autoParam α tactic = α

Helper functions for manipulating interpolated strings

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

Equations

• Lean.Syntax.isInterpolatedStrLit? stx = 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

• Lean.Syntax.getSepArgs stx = Array.getSepElems (Lean.Syntax.getArgs stx)

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 : Lean.Term) (toTypeFn : Lean.Term) : Lean.MacroM Lean.Term

Equations

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

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

Equations

• Lean.Meta.instInhabitedTransparencyMode = { default := Lean.Meta.TransparencyMode.all }

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

Equations

• Lean.Meta.instBEqTransparencyMode = { beq := Lean.Meta.beqTransparencyMode✝ }

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

Equations

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

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

Equations

• Lean.Meta.instInhabitedEtaStructMode = { default := Lean.Meta.EtaStructMode.all }

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

Equations

• Lean.Meta.instBEqEtaStructMode = { beq := Lean.Meta.beqEtaStructMode✝ }

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

Equations

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

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

Equations

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

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

Equations

• Lean.Meta.DSimp.instBEqConfig = { beq := Lean.Meta.DSimp.beqConfig✝ }

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

Equations

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

def Lean.Meta.Simp.defaultMaxSteps : Nat

Equations

• Lean.Meta.Simp.defaultMaxSteps = 100000

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

Equations

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

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

Equations

• Lean.Meta.Simp.instBEqConfig = { beq := Lean.Meta.Simp.beqConfig✝ }

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

Equations

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

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

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

Equations

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

inductive Lean.Meta.Occurrences : Type

• all: Lean.Meta.Occurrences
• pos: List Nat → Lean.Meta.Occurrences
• neg: List Nat → Lean.Meta.Occurrences

instance Lean.Meta.instInhabitedOccurrences : Inhabited Lean.Meta.Occurrences

Equations

• Lean.Meta.instInhabitedOccurrences = { default := Lean.Meta.Occurrences.all }

instance Lean.Meta.instBEqOccurrences : BEq Lean.Meta.Occurrences

Equations

• Lean.Meta.instBEqOccurrences = { beq := Lean.Meta.beqOccurrences✝ }

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

Equations

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

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

Equations

• Lean.Meta.Occurrences.isAll x = match x with | Lean.Meta.Occurrences.all => true | x => false

structure Lean.Meta.Rewrite.Config : Type

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

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

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