Init.Meta

Lean.Syntax.getSubstring? stx withLeading withTrailing = let _discr := Lean.Syntax.getTailInfo stx; match Lean.Syntax.getHeadInfo stx, Lean.Syntax.getTailInfo stx with | Lean.SourceInfo.original lead startPos trailing endPos, Lean.SourceInfo.original leading pos trail stopPos => some { str := lead.str, startPos := if withLeading = true then lead.startPos else startPos, stopPos := if withTrailing = true then trail.stopPos else stopPos } | x, x_1 => none

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

source

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

Lean.Syntax → Option Lean.Syntax

source

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

source

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

Lean.Syntax

Equations

Lean.Syntax.unsetTrailing stx = match Lean.Syntax.getTailInfo stx with | Lean.SourceInfo.original lead pos trailing endPos => Lean.Syntax.setTailInfo stx (Lean.SourceInfo.original lead pos (String.toSubstring "") endPos) | x => stx

source

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

Lean.Syntax → Option Lean.Syntax

source

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

source

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

Lean.Syntax → Lean.Syntax

Equations

Lean.Syntax.setInfo info _fun_discr = match _fun_discr with | Lean.Syntax.atom info val => Lean.Syntax.atom info val | Lean.Syntax.ident info rawVal val pre => Lean.Syntax.ident info rawVal val pre | Lean.Syntax.node info kind args => Lean.Syntax.node info kind args | Lean.Syntax.missing => Lean.Syntax.missing

source

partial def Lean.Syntax.getHead? :

Lean.Syntax → Option Lean.Syntax

Return the first atom/identifier that has position information

source

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)

source

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

Lean.Syntax

Equations

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

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

source

@[inline]

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

m α

Equations

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

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

source

@[inline]

def Lean.mkNode (k : Lean.SyntaxNodeKind) (args : Array Lean.Syntax) :

Lean.Syntax

Equations

Lean.mkNode k args = Lean.Syntax.node Lean.SourceInfo.none k args

source

structure Lean.Module :

Type

header : Lean.Syntax
commands : Array Lean.Syntax

source

partial def Lean.expandMacros :

Lean.Syntax → Lean.MacroM Lean.Syntax

Expand all macros in the given syntax

source

def Lean.mkIdentFrom (src : Lean.Syntax) (val : Lean.Name) :

Lean.Syntax

Equations

Lean.mkIdentFrom src val = Lean.Syntax.ident (Lean.SourceInfo.fromRef src) (String.toSubstring (toString val)) val []

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

source

def Lean.mkIdentFromRef {m : Type → Type} [inst : Monad m] [inst : Lean.MonadRef m] (val : Lean.Name) :

m Lean.Syntax

Equations

Lean.mkIdentFromRef val = do let a ← Lean.getRef pure (Lean.mkIdentFrom a val)

source

def Lean.mkCIdentFrom (src : Lean.Syntax) (c : Lean.Name) :

Lean.Syntax

Equations

Lean.mkCIdentFrom src c = let id := Lean.addMacroScope `_internal c Lean.reservedMacroScope; Lean.Syntax.ident (Lean.SourceInfo.fromRef src) (String.toSubstring (toString id)) id [(c, [])]

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.

source

def Lean.mkCIdentFromRef {m : Type → Type} [inst : Monad m] [inst : Lean.MonadRef m] (c : Lean.Name) :

m Lean.Syntax

Equations

Lean.mkCIdentFromRef c = do let a ← Lean.getRef pure (Lean.mkCIdentFrom a c)

source

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

Lean.Syntax

Equations

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

source

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

Lean.Syntax

Equations

Lean.mkIdent val = Lean.Syntax.ident Lean.SourceInfo.none (String.toSubstring (toString val)) val []

source

@[inline]

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

Lean.Syntax

Equations

Lean.mkNullNode args = Lean.mkNode Lean.nullKind args

source

@[inline]

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

Lean.Syntax

Equations

Lean.mkGroupNode args = Lean.mkNode Lean.groupKind args

source

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

Array Lean.Syntax

Equations

Lean.mkSepArray as sep = Id.run (let i := 0; let r := #[]; do let r ← forIn as { fst := i, snd := r } fun a r => let i := r.fst; let r := r.snd; let _do_jp := fun i r y => let i := i + 1; do pure PUnit.unit pure (ForInStep.yield { fst := i, snd := r }); if i > 0 then let r := Array.push (Array.push r sep) a; do let y ← pure PUnit.unit _do_jp i r y else let r := Array.push r a; do let y ← pure PUnit.unit _do_jp i r y match r with | { fst := i, snd := r } => pure r)

source

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

Lean.Syntax

Equations

Lean.mkOptionalNode arg = match arg with | some arg => Lean.mkNullNode #[arg] | none => Lean.mkNullNode

source

def Lean.mkHole (ref : Lean.Syntax) :

Lean.Syntax

Equations

Lean.mkHole ref = Lean.mkNode `Lean.Parser.Term.hole #[Lean.mkAtomFrom ref "_"]

source

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)

source

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 (Lean.mkAtom sep) }

source

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

m (Lean.Syntax.SepArray sep)

Equations

Lean.Syntax.SepArray.ofElemsUsingRef elems = do let ref ← Lean.getRef pure { elemsAndSeps := Lean.mkSepArray elems (Lean.mkAtomFrom ref sep) }

source

instance Lean.Syntax.instCoeArraySyntaxSepArray (sep : String) :

Coe (Array Lean.Syntax) (Lean.Syntax.SepArray sep)

Equations

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

source

def Lean.Syntax.mkApp (fn : Lean.Syntax) (args : Array Lean.Syntax) :

Lean.Syntax

Equations

Lean.Syntax.mkApp fn _fun_discr = match _fun_discr with | #[] => fn | args => Lean.mkNode `Lean.Parser.Term.app #[fn, Lean.mkNullNode args]

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

source

def Lean.Syntax.mkCApp (fn : Lean.Name) (args : Array Lean.Syntax) :

Lean.Syntax

Equations

Lean.Syntax.mkCApp fn args = Lean.Syntax.mkApp (Lean.mkCIdent fn) args

source

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

Lean.Syntax

Equations

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

source

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

Lean.Syntax

Equations

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

source

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

Lean.Syntax

Equations

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

source

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

Lean.Syntax

Equations

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

source

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

Lean.Syntax

Equations

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

source

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

Option Nat

Equations

Lean.Syntax.decodeNatLitVal? s = let len := String.length s; if (len == 0) = true then none else let c := String.get s 0; if (c == Char.ofNat 48) = true then if (len == 1) = true then some 0 else let c := String.get s { byteIdx := 1 }; if (c == Char.ofNat 120 || c == Char.ofNat 88) = true then Lean.Syntax.decodeHexLitAux s { byteIdx := 2 } 0 else if (c == Char.ofNat 98 || c == Char.ofNat 66) = true then Lean.Syntax.decodeBinLitAux s { byteIdx := 2 } 0 else if (c == Char.ofNat 111 || c == Char.ofNat 79) = true then Lean.Syntax.decodeOctalLitAux s { byteIdx := 2 } 0 else if Char.isDigit c = true then Lean.Syntax.decodeDecimalLitAux s 0 0 else none else if Char.isDigit c = true then Lean.Syntax.decodeDecimalLitAux s 0 0 else none

source

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

Option String

Equations

Lean.Syntax.isLit? litKind stx = match stx with | Lean.Syntax.node info k args => if (k == litKind && Array.size args == 1) = true then match Array.get! args 0 with | Lean.Syntax.atom info val => some val | x => none else none | x => none

source

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

Option Nat

Equations

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

source

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

Option Nat

Equations

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

source

def Lean.Syntax.decodeScientificLitVal? (s : String) :

Option (Nat × Bool × Nat)

Equations

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

source

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

Option (Nat × Bool × Nat)

source

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

Option (Nat × Bool × Nat)

Equations

Lean.Syntax.decodeScientificLitVal?.decodeExp s i val e = let c := String.get s i; if (c == Char.ofNat 45) = true then Lean.Syntax.decodeScientificLitVal?.decodeAfterExp s (String.next s i) val e true 0 else Lean.Syntax.decodeScientificLitVal?.decodeAfterExp s i val e false 0

source

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

Option (Nat × Bool × Nat)

source

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

Option (Nat × Bool × Nat)

source

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

source

def Lean.Syntax.isIdOrAtom? :

Lean.Syntax → Option String

Equations

Lean.Syntax.isIdOrAtom? _fun_discr = match _fun_discr with | Lean.Syntax.atom info val => some val | Lean.Syntax.ident info rawVal val preresolved => some (Substring.toString rawVal) | x => none

source

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

Nat

Equations

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

source

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

Option (Char × String.Pos)

Equations

Lean.Syntax.decodeQuotedChar s i = let c := String.get s i; let i := String.next s i; if (c == Char.ofNat 92) = true then pure (Char.ofNat 92, i) else if c = Char.ofNat 34 then pure (Char.ofNat 34, i) else if c = Char.ofNat 39 then pure (Char.ofNat 39, i) else if c = Char.ofNat 114 then pure (Char.ofNat 13, i) else if c = Char.ofNat 110 then pure (Char.ofNat 10, i) else if c = Char.ofNat 116 then pure (Char.ofNat 9, i) else if c = Char.ofNat 120 then do let discr ← Lean.Syntax.decodeHexDigit s i match discr with | (d₁, i) => do let discr ← Lean.Syntax.decodeHexDigit s i match discr with | (d₂, i) => pure (Char.ofNat (16 * d₁ + d₂), i) else if c = Char.ofNat 117 then do let discr ← Lean.Syntax.decodeHexDigit s i match discr with | (d₁, i) => do let discr ← Lean.Syntax.decodeHexDigit s i match discr with | (d₂, i) => do let discr ← Lean.Syntax.decodeHexDigit s i match discr with | (d₃, i) => do let discr ← Lean.Syntax.decodeHexDigit s i match discr with | (d₄, i) => pure (Char.ofNat (16 * (16 * (16 * d₁ + d₂) + d₃) + d₄), i) else none

source

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

Option String

source

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

Option String

Equations

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

source

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

source

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

Option Char

Equations

Lean.Syntax.decodeCharLit s = let c := String.get s { byteIdx := 1 }; if (c == Char.ofNat 92) = true then do let discr ← Lean.Syntax.decodeQuotedChar s { byteIdx := 2 } match discr with | (c, snd) => pure c else pure c

source

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

source

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

List Substring

Equations

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

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

source

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

Option Lean.Name

Equations

Lean.Syntax.decodeNameLit s = if (String.get s 0 == Char.ofNat 96) = true then match Lean.Syntax.splitNameLitAux (Substring.drop (String.toSubstring s) 1) [] with | [] => none | comps => some (List.foldr (fun comp n => let comp := Substring.toString comp; if Lean.isIdBeginEscape (String.front comp) = true then Lean.Name.mkStr n (String.dropRight (String.drop comp 1) 1) else if Char.isDigit (String.front comp) = true then match Lean.Syntax.decodeNatLitVal? comp with | some k => Lean.Name.mkNum n k | x => panicWithPosWithDecl "Init.Meta" "Lean.Syntax.decodeNameLit" 723 12 "unreachable code has been reached" else Lean.Name.mkStr n comp) Lean.Name.anonymous comps) else none

source

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

Option Lean.Name

Equations

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

source

def Lean.Syntax.hasArgs :

Lean.Syntax → Bool

Equations

Lean.Syntax.hasArgs _fun_discr = match _fun_discr with | Lean.Syntax.node info kind args => decide (Array.size args > 0) | x => false

source

def Lean.Syntax.isAtom :

Lean.Syntax → Bool

Equations

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

source

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

Lean.Syntax → Bool

Equations

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

source

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

source

def Lean.Syntax.getOptional? (stx : Lean.Syntax) :

Option Lean.Syntax

Equations

Lean.Syntax.getOptional? stx = match stx with | Lean.Syntax.node info k args => if (k == Lean.nullKind && Array.size args == 1) = true then some (Array.get! args 0) else none | x => none

source

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

Option Lean.Name

Equations

Lean.Syntax.getOptionalIdent? stx = match Lean.Syntax.getOptional? stx with | some stx => some (Lean.Syntax.getId stx) | none => none

source

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

Lean.Syntax → Option Lean.Syntax

source

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

source

class Lean.Quote (α : Type) :

Type

quote : α → Lean.Syntax

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

Instances

source

instance Lean.instQuoteSyntax :

Lean.Quote Lean.Syntax

Equations

Lean.instQuoteSyntax = { quote := id }

source

instance Lean.instQuoteBool :

Lean.Quote Bool

Equations

Lean.instQuoteBool = { quote := fun _fun_discr => match _fun_discr with | true => Lean.mkCIdent `Bool.true | false => Lean.mkCIdent `Bool.false }

source

instance Lean.instQuoteString :

Lean.Quote String

Equations

Lean.instQuoteString = { quote := fun val => Lean.Syntax.mkStrLit val }

source

instance Lean.instQuoteNat :

Lean.Quote Nat

Equations

Lean.instQuoteNat = { quote := fun n => Lean.Syntax.mkNumLit (toString n) }

source

instance Lean.instQuoteSubstring :

Lean.Quote Substring

Equations

Lean.instQuoteSubstring = { quote := fun s => Lean.Syntax.mkCApp `String.toSubstring #[Lean.quote (Substring.toString s)] }

source

instance Lean.instQuoteName :

Lean.Quote Lean.Name

Equations

Lean.instQuoteName = { quote := fun n => match Lean.getEscapedNameParts? [] n with | some ss => Lean.mkNode `Lean.Parser.Term.quotedName #[Lean.Syntax.mkNameLit ("`" ++ String.intercalate "." ss)] | none => Lean.quoteNameMk n }

source

instance Lean.instQuoteProd {α : Type} {β : Type} [inst : Lean.Quote α] [inst : Lean.Quote β] :

Lean.Quote (α × β)

Equations

Lean.instQuoteProd = { quote := fun _fun_discr => match _fun_discr with | (a, b) => Lean.Syntax.mkCApp `Prod.mk #[Lean.quote a, Lean.quote b] }

source

instance Lean.instQuoteList {α : Type} [inst : Lean.Quote α] :

Lean.Quote (List α)

Equations

Lean.instQuoteList = { quote := Lean.quoteList }

source

instance Lean.instQuoteArray {α : Type} [inst : Lean.Quote α] :

Lean.Quote (Array α)

Equations

Lean.instQuoteArray = { quote := fun xs => Lean.Syntax.mkCApp `List.toArray #[Lean.quote (Array.toList xs)] }

source

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

Lean.Quote (Option α)

Equations

Lean.Option.hasQuote = { quote := Lean.quoteOption }

source

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

Lean.MacroM Nat

Equations

Lean.evalPrec stx = Lean.Macro.withIncRecDepth stx do let stx ← Lean.expandMacros stx let discr : Lean.Syntax := stx cond (Lean.Syntax.isOfKind discr `num) (let num := discr; pure (Option.getD (Lean.Syntax.isNatLit? num) 0)) (let discr := stx; Lean.Macro.throwErrorAt stx "unexpected precedence")

source

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

source

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

Lean.MacroM Nat

Equations

Lean.evalPrio stx = Lean.Macro.withIncRecDepth stx do let stx ← Lean.expandMacros stx let discr : Lean.Syntax := stx cond (Lean.Syntax.isOfKind discr `num) (let num := discr; pure (Option.getD (Lean.Syntax.isNatLit? num) 0)) (let discr := stx; Lean.Macro.throwErrorAt stx "unexpected priority")

source

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

source

def Lean.evalOptPrio :

Option Lean.Syntax → Lean.MacroM Nat

Equations

Lean.evalOptPrio _fun_discr = match _fun_discr with | some prio => Lean.evalPrio prio | none => pure 1000

source

@[inline]

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

Array α

Equations

@Array.getSepElems = @Array.getEvenElems

source

def Array.filterSepElemsM {m : Type → Type} [inst : 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 #[]

source

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)

source

def Array.mapSepElemsM {m : Type → Type} [inst : 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 #[]

source

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)

source

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

source

instance Lean.Syntax.SepArray.instCoeTailSepArrayArraySyntax (sep : String) :

CoeTail (Lean.Syntax.SepArray sep) (Array Lean.Syntax)

Equations

Lean.Syntax.SepArray.instCoeTailSepArrayArraySyntax sep = { coe := Lean.Syntax.SepArray.getElems }

source

@[inline]

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

Sort u

Equations

autoParam α tactic = α

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.

source

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

source

def Lean.Syntax.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

Lean.Syntax.expandInterpolatedStrChunks chunks mkAppend mkElem = let i := 0; let result := Lean.Syntax.missing; do let r ← forIn chunks { fst := i, snd := result } fun elem r => let i := r.fst; let result := r.snd; let _do_jp := fun i result elem => let _do_jp := fun i result y => let i := i + 1; do pure PUnit.unit pure (ForInStep.yield { fst := i, snd := result }); if (i == 0) = true then let result := elem; do let y ← pure PUnit.unit _do_jp i result y else do let r ← mkAppend result elem let result : Lean.Syntax := r let y ← pure PUnit.unit _do_jp i result y; match Lean.Syntax.isInterpolatedStrLit? elem with | none => do let y ← mkElem elem _do_jp i result y | some str => do let y ← mkElem (Lean.Syntax.mkStrLit str) _do_jp i result y match r with | { fst := i, snd := result } => pure result

source

def Lean.Syntax.expandInterpolatedStr (interpStr : Lean.Syntax) (type : Lean.Syntax) (toTypeFn : Lean.Syntax) :

Lean.MacroM Lean.Syntax

Equations

Lean.Syntax.expandInterpolatedStr interpStr type toTypeFn = do let r ← Lean.Syntax.expandInterpolatedStrChunks (Lean.Syntax.getArgs interpStr) (fun a b => do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `«term_++_» #[a, Lean.Syntax.atom info "++", b])) fun a => do let _ ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[toTypeFn, Lean.Syntax.node Lean.SourceInfo.none `null #[a]]) let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[r, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeAscription #[Lean.Syntax.atom info ":", type]]], Lean.Syntax.atom info ")"])

source

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

Array Lean.Syntax

Equations

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

source

inductive Lean.Meta.TransparencyMode :

Type

source

instance Lean.Meta.instInhabitedTransparencyMode :

Inhabited Lean.Meta.TransparencyMode

Equations

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

source

instance Lean.Meta.instBEqTransparencyMode :

BEq Lean.Meta.TransparencyMode

Equations

Lean.Meta.instBEqTransparencyMode = { beq := [anonymous] }

source

instance Lean.Meta.instReprTransparencyMode :

Repr Lean.Meta.TransparencyMode

Equations

Lean.Meta.instReprTransparencyMode = { reprPrec := [anonymous] }

source

inductive Lean.Meta.EtaStructMode :

Type

source

instance Lean.Meta.instInhabitedEtaStructMode :

Inhabited Lean.Meta.EtaStructMode

Equations

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

source

instance Lean.Meta.instBEqEtaStructMode :

BEq Lean.Meta.EtaStructMode

Equations

Lean.Meta.instBEqEtaStructMode = { beq := [anonymous] }

source

instance Lean.Meta.instReprEtaStructMode :

Repr Lean.Meta.EtaStructMode

Equations

Lean.Meta.instReprEtaStructMode = { reprPrec := [anonymous] }

source

structure Lean.Meta.DSimp.Config :

Type

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

source

instance Lean.Meta.DSimp.instInhabitedConfig :

Inhabited Lean.Meta.DSimp.Config

Equations

Lean.Meta.DSimp.instInhabitedConfig = { default := { zeta := default, beta := default, eta := default, etaStruct := default, iota := default, proj := default, decide := default, autoUnfold := default } }

source

instance Lean.Meta.DSimp.instBEqConfig :

BEq Lean.Meta.DSimp.Config

Equations

Lean.Meta.DSimp.instBEqConfig = { beq := [anonymous] }

source

instance Lean.Meta.DSimp.instReprConfig :

Repr Lean.Meta.DSimp.Config

Equations

Lean.Meta.DSimp.instReprConfig = { reprPrec := [anonymous] }

source

def Lean.Meta.Simp.defaultMaxSteps :

Nat

Equations

Lean.Meta.Simp.defaultMaxSteps = 100000

source

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

source

instance Lean.Meta.Simp.instInhabitedConfig :

Inhabited Lean.Meta.Simp.Config

Equations

Lean.Meta.Simp.instInhabitedConfig = { default := { maxSteps := default, maxDischargeDepth := default, contextual := default, memoize := default, singlePass := default, zeta := default, beta := default, eta := default, etaStruct := default, iota := default, proj := default, decide := default, arith := default, autoUnfold := default } }