def DY.Meta.CombineMacro.explicitNameOfBracketedBinder (stx : Lean.TSyntax `Lean.Parser.Term.bracketedBinder) : Lean.TSyntaxArray `ident

Equations

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

def Lean.Parser.Category.combine_from : Category

Equations

• Lean.Parser.Category.combine_from = { }

def DY.Meta.CombineMacro.combine_from.quot : Lean.ParserDescr

Equations

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

def DY.Meta.CombineMacro.combine_from__ : Lean.ParserDescr

Equations

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

def DY.Meta.CombineMacro.combine_into.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.combine_into : Category

Equations

• Lean.Parser.Category.combine_into = { }

def DY.Meta.CombineMacro.combine_into__ : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.combine_option : Category

Equations

• Lean.Parser.Category.combine_option = { }

def DY.Meta.CombineMacro.combine_option.quot : Lean.ParserDescr

Equations

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

def DY.Meta.CombineMacro.«combine_option+toplevel» : Lean.ParserDescr

Equations

• DY.Meta.CombineMacro.«combine_option+toplevel» = Lean.ParserDescr.node `DY.Meta.CombineMacro.«combine_option+toplevel» 1024 (Lean.ParserDescr.symbol "+toplevel ")

def DY.Meta.CombineMacro.«command#combine_one__From_» : Lean.ParserDescr

Equations

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

def DY.Meta.CombineMacro.«command#combine__Into_From_» : Lean.ParserDescr

Equations

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

structure DY.Meta.CombineMacro.CombineExplicitConfig : Type

• name : Lean.Name
• combineName : Lean.Name
• internalOutTypeStx (args : Lean.TSyntaxArray `term) (id : Lean.TSyntax `term) : Lean.MacroM (Lean.TSyntax `term)
• outTypeStx (args : Lean.TSyntaxArray `term) : Lean.MacroM (Lean.TSyntax `term)
• isTheorem : Bool

structure DY.Meta.CombineMacro.CombineExplicitSimpleConfig : Type

• name : Lean.Name
• refereeName : Lean.Name
• combineName : Lean.Name
• outTypeName : Lean.Name
• isTheorem : Bool

def DY.Meta.CombineMacro.CombineExplicitConfig.makeSimple (config : CombineExplicitSimpleConfig) : CombineExplicitConfig

Equations

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

def DY.Meta.CombineMacro.combineExplicit (params : Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder) (sources : Lean.TSyntaxArray `combine_from) (config : CombineExplicitConfig) : Lean.MacroM (Lean.TSyntaxArray `command)

Equations

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

structure DY.Meta.CombineMacro.CombineTypeclassConfig : Type

• internalIdStx (args : Lean.TSyntaxArray `term) (id : Lean.TSyntax `term) : Lean.MacroM (Lean.TSyntax `term)
• internalStx (name : Lean.TSyntax `ident) (args : Lean.TSyntaxArray `term) : Lean.MacroM (Lean.TSyntax `term)
• combineStx (args : Lean.TSyntaxArray `term) : Lean.MacroM (Lean.TSyntax `term)
• finalStx (args : Lean.TSyntaxArray `term) : Lean.MacroM (Lean.TSyntax `term)
• useInferInstanceAs : Bool

structure DY.Meta.CombineMacro.CombineTypeclassSimpleConfig : Type

• refereeName : Lean.Name
• refereeInternalName : Lean.Name
• combineName : Lean.Name
• outTypeName : Lean.Name
• useInferInstanceAs : Bool

def DY.Meta.CombineMacro.CombineTypeclassConfig.makeSimple (config : CombineTypeclassSimpleConfig) : CombineTypeclassConfig

Equations

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

def DY.Meta.CombineMacro.combineTypeclass (params : Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder) (sources : Lean.TSyntaxArray `combine_from) (config : CombineTypeclassConfig) : Lean.MacroM (Lean.TSyntaxArray `command)

Equations

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

structure DY.Meta.CombineMacro.HasStepConfig : Type

• sourceInstanceStx (args : Lean.TSyntaxArray `term) (id : Lean.TSyntax `term) : Lean.MacroM (Lean.TSyntax `term)
• targetInstanceStx (name : Lean.TSyntax `ident) (argsSource argsTarget : Lean.TSyntaxArray `term) : Lean.MacroM (Lean.TSyntax `term)

structure DY.Meta.CombineMacro.HasStepSimpleConfig : Type

• name : Lean.Name
• internalName : Lean.Name
• combineName : Lean.Name
• hasStepName : Lean.Name

def DY.Meta.CombineMacro.HasStepConfig.makeSimple (config : HasStepSimpleConfig) : HasStepConfig

Equations

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

def DY.Meta.CombineMacro.mkHasStep (params : Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder) (sources : Lean.TSyntaxArray `combine_from) (config : HasStepConfig) : Lean.MacroM (Lean.TSyntaxArray `command)

Equations

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

structure DY.Meta.CombineMacro.HasCombineConfig : Type

• hasCombineStx (args : Lean.TSyntaxArray `term) : Lean.MacroM (Lean.TSyntax `term)
• hasStx (args : Lean.TSyntaxArray `term) : Lean.MacroM (Lean.TSyntax `term)

def DY.Meta.CombineMacro.mkHasCombine (params : Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder) (config : HasCombineConfig) : Lean.MacroM (Lean.TSyntaxArray `command)

Equations

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

structure DY.Meta.CombineMacro.Options : Type

• toplevel : Bool

def DY.Meta.CombineMacro.parseOptions (options : Lean.TSyntaxArray `combine_option) : Options

Equations

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