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 x x_1, Lean.SourceInfo.original x_2 x_3 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

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 trail 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 x = match x with | Lean.Syntax.atom x val => Lean.Syntax.atom info val | Lean.Syntax.ident x rawVal val pre => Lean.Syntax.ident info rawVal val pre | Lean.Syntax.node x 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

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

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

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

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

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, [])]

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 := r, snd := i } fun a r => let r_1 := r.fst; let i := r.snd; let _do_jp := fun r i y => let i := i + 1; do pure PUnit.unit pure (ForInStep.yield { fst := r, snd := i }); if i > 0 then let r := Array.push (Array.push r_1 sep) a; do let y ← pure PUnit.unit _do_jp r i y else let r := Array.push r_1 a; do let y ← pure PUnit.unit _do_jp r i y let x : MProd (Array Lean.Syntax) Nat := r match x with | { fst := r, snd := i } => 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 x = match x with | #[] => fn | args => Lean.mkNode `Lean.Parser.Term.app #[fn, Lean.mkNullNode args]

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 1; if (c == Char.ofNat 120 || c == Char.ofNat 88) = true then Lean.Syntax.decodeHexLitAux s 2 0 else if (c == Char.ofNat 98 || c == Char.ofNat 66) = true then Lean.Syntax.decodeBinLitAux s 2 0 else if (c == Char.ofNat 111 || c == Char.ofNat 79) = true then Lean.Syntax.decodeOctalLitAux s 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 x k args => if (k == litKind && Array.size args == 1) = true then match Array.get! args 0 with | Lean.Syntax.atom x 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 = (fun decodeAfterExp decodeAfterDot decode => let len := String.length s; if (len == 0) = true then none else let c := String.get s 0; if Char.isDigit c = true then decode 0 0 else none) (Lean.Syntax.decodeScientificLitVal?.decodeAfterExp s) (Lean.Syntax.decodeScientificLitVal?.decodeExp s) (Lean.Syntax.decodeScientificLitVal?.decodeAfterDot s) (Lean.Syntax.decodeScientificLitVal?.decode s)

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? x = match x with | Lean.Syntax.atom x val => some val | Lean.Syntax.ident x rawVal x_1 x_2 => 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 = OptionM.run (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 let x : Nat × String.Pos := discr match x with | (d₁, i) => do let discr ← Lean.Syntax.decodeHexDigit s i let x : Nat × String.Pos := discr match x 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 let x : Nat × String.Pos := discr match x with | (d₁, i) => do let discr ← Lean.Syntax.decodeHexDigit s i let x : Nat × String.Pos := discr match x with | (d₂, i) => do let discr ← Lean.Syntax.decodeHexDigit s i let x : Nat × String.Pos := discr match x with | (d₃, i) => do let discr ← Lean.Syntax.decodeHexDigit s i let x : Nat × String.Pos := discr match x 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 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 = OptionM.run (let c := String.get s 1; if (c == Char.ofNat 92) = true then do let discr ← Lean.Syntax.decodeQuotedChar s 2 let x : Char × String.Pos := discr match x with | (c, x) => 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 [])

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" 719 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 x = match x with | Lean.Syntax.node x x_1 args => decide (Array.size args > 0) | x => false

source

def Lean.Syntax.isAtom :

Lean.Syntax → Bool

Equations

Lean.Syntax.isAtom x = match x with | Lean.Syntax.atom x x_1 => true | x => false

source

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

Lean.Syntax → Bool

Equations

Lean.Syntax.isToken token x = match x with | Lean.Syntax.atom x 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 x 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 x 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

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 x => match x 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 x => match x 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 `numLit) (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 `numLit) (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 x = match x 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 = α

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 let x : MProd Nat Lean.Syntax := r match x 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 = let ref := interpStr; 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

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 : Bool
iota : Bool
proj : Bool
decide : Bool

source

instance Lean.Meta.Simp.instBEqConfig :

BEq Lean.Meta.Simp.Config

Equations

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

source

instance Lean.Meta.Simp.instReprConfig :

Repr Lean.Meta.Simp.Config

Equations

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

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

source

structure Lean.Meta.Simp.ConfigCtx extends Lean.Meta.Simp.Config :

Type

source

def Lean.Meta.Simp.neutralConfig :

Lean.Meta.Simp.Config

Equations

Lean.Meta.Simp.neutralConfig = { maxSteps := Lean.Meta.Simp.defaultMaxSteps, maxDischargeDepth := 2, contextual := false, memoize := true, singlePass := false, zeta := false, beta := false, eta := false, etaStruct := true, iota := false, proj := false, decide := false }

source

structure Lean.Meta.Rewrite.Config :

Type

transparency : Lean.Meta.TransparencyMode
offsetCnstrs : Bool

source

def Lean.Parser.Tactic.tacticErw__ :

Lean.ParserDescr

Equations

Lean.Parser.Tactic.tacticErw__ = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticErw__ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "erw " false) Lean.Parser.Tactic.rwRuleSeq) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.location))