Init.Meta

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.

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

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

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

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

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

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)

source

@[inline]

def Lean.withHeadRefOnly {m : Type → Type} [inst : Monad m] [inst : 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 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.TSyntax k

Equations

Lean.mkNode k args = { raw := 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.Ident

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

Equations

Lean.mkIdentFrom src val = { raw := 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.Ident

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

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

source

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

Lean.Ident

Equations

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

source

@[export lean_mk_syntax_ident]

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

Lean.Ident

Equations

Lean.mkIdent val = { raw := 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).raw

source

@[inline]

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

Lean.Syntax

Equations

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

source

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.

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 "_"]).raw

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 (if String.isEmpty sep = true then Lean.mkNullNode else 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

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

source

instance Lean.Syntax.instCoeArraySyntaxSepArray {sep : String} :

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

Equations

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

source

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

source

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 _fun_discr = match _fun_discr with | #[] => fn | args => { raw := (Lean.mkNode `Lean.Parser.Term.app #[fn.raw, Lean.mkNullNode (Lean.TSyntaxArray.raw args)]).raw }

source

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

Lean.Term

Equations

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

source

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]

source

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

source

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

source

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

source

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

source

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

Option Nat

Equations

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

source

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.

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

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

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

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

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

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

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

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

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

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

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

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

source

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

Option Lean.Name

Equations

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

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

def Lean.TSyntax.getNat (s : Lean.TSyntax Lean.numLitKind) :

Nat

Equations

Lean.TSyntax.getNat s = Option.get! (Lean.Syntax.isNatLit? s.raw)

source

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

Lean.Name

Equations

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

source

def Lean.TSyntax.getString (s : Lean.TSyntax Lean.strLitKind) :

String

Equations

Lean.TSyntax.getString s = Option.get! (Lean.Syntax.isStrLit? s.raw)

source

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

source

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

Type

quote : α → Lean.TSyntax k

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

Instances

source

instance Lean.instQuote {α : Type} {k : Lean.SyntaxNodeKind} {k' : Lean.SyntaxNodeKind} [inst : Lean.Quote α k] [inst : 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)

source

instance Lean.instQuoteTermMkStrAnonymous:

Lean.Quote Lean.Term

Equations

Lean.instQuoteTermMkStrAnonymous = Lean.Quote.mk `term id

source

instance Lean.instQuoteBoolMkStrAnonymous:

Lean.Quote Bool

Equations

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

source

instance Lean.instQuoteStringStrLitKind:

Lean.Quote String Lean.strLitKind

Equations

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

source

instance Lean.instQuoteNatNumLitKind:

Lean.Quote Nat Lean.numLitKind

Equations

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

source

instance Lean.instQuoteSubstringMkStrAnonymous:

Lean.Quote Substring

Equations

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

source

def Lean.quoteNameMk:

Lean.Name → Lean.Term

Equations

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

source

instance Lean.instQuoteNameMkStrAnonymous:

Lean.Quote Lean.Name

Equations

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

source

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

Lean.Quote (α × β)

Equations

Lean.instQuoteProdMkStrAnonymous = Lean.Quote.mk `term fun x => match x with | (a, b) => Lean.Syntax.mkCApp `Prod.mk #[Lean.quote `term a, Lean.quote `term b]

source

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

Lean.Quote (List α)

Equations

Lean.instQuoteListMkStrAnonymous = Lean.Quote.mk `term Lean.quoteList

source

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

Lean.Quote (Array α)

Equations

Lean.instQuoteArrayMkStrAnonymous = Lean.Quote.mk `term fun xs => Lean.Syntax.mkCApp `List.toArray #[Lean.quote `term (Array.toList xs)]

source

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

Lean.Quote (Option α)

Equations

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

source

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

Lean.MacroM Nat

Equations

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

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

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

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.TSyntax `prio) → Lean.MacroM Nat

Equations

Lean.evalOptPrio _fun_discr = match _fun_discr with | some prio => Lean.evalPrio prio.raw | 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

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)

source

instance Lean.Syntax.instCoeTailSepArrayArraySyntax {sep : String} :

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

Equations

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

source

instance Lean.Syntax.instCoeTSepArrayTSyntaxArray {k : Lean.SyntaxNodeKinds} {sep : String} :

Coe (Lean.Syntax.TSepArray k sep) (Lean.TSyntaxArray k)

Equations

Lean.Syntax.instCoeTSepArrayTSyntaxArray = { coe := Lean.Syntax.TSepArray.getElems }

source

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

Coe (Lean.TSyntaxArray k) (Lean.TSyntaxArray k')

Equations

Lean.Syntax.instCoeTSyntaxArray = { coe := fun a => Lean.TSyntaxArray.mk (Lean.TSyntaxArray.raw a) }

source

instance Lean.Syntax.instCoeTSyntaxArrayArraySyntax {k : Lean.SyntaxNodeKinds} :

Coe (Lean.TSyntaxArray k) (Array Lean.Syntax)

Equations

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

source

instance Lean.Syntax.instCoeIdentTSyntaxConsSyntaxNodeKindMkStrAnonymousNil:

Coe Lean.Ident (Lean.TSyntax `Lean.Parser.Command.declId)

Equations

Lean.Syntax.instCoeIdentTSyntaxConsSyntaxNodeKindMkStrAnonymousNil = { coe := fun id => Lean.mkNode `Lean.Parser.Command.declId #[id.raw, Lean.mkNullNode] }

source

instance Lean.Syntax.instCoeTermTSyntaxConsSyntaxNodeKindMkStrAnonymousNil:

Coe Lean.Term (Lean.TSyntax `Lean.Parser.Term.funBinder)

Equations

Lean.Syntax.instCoeTermTSyntaxConsSyntaxNodeKindMkStrAnonymousNil = { coe := fun stx => { raw := stx.raw } }

source

@[inline]

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