structure StrataDDM.Elab.ArgElaborator : Type

Describes an elaboration relationship between a argument in the bindings and the syntax node.

• syntaxLevel : Nat
• argLevel : Nat
• contextLevel : Option (Fin self.argLevel)
• scopeTVar : Option (Fin self.argLevel)

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedArgElaborator : Inhabited ArgElaborator

Equations

• StrataDDM.Elab.instInhabitedArgElaborator = { default := StrataDDM.Elab.instInhabitedArgElaborator.default }

def StrataDDM.Elab.instInhabitedArgElaborator.default : ArgElaborator

Equations

• StrataDDM.Elab.instInhabitedArgElaborator.default = { syntaxLevel := default, argLevel := default, contextLevel := default, scopeTVar := default }

def StrataDDM.Elab.instReprArgElaborator.repr : ArgElaborator → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance StrataDDM.Elab.instReprArgElaborator : Repr ArgElaborator

Equations

• StrataDDM.Elab.instReprArgElaborator = { reprPrec := StrataDDM.Elab.instReprArgElaborator.repr }

@[reducible, inline]

abbrev StrataDDM.Elab.ArgElaboratorArray (sc : Nat) : Type

Equations

• StrataDDM.Elab.ArgElaboratorArray sc = Array { a : StrataDDM.Elab.ArgElaborator // a.syntaxLevel < sc }

structure StrataDDM.Elab.SyntaxElaborator : Type

Information needed to elaborate operations or functions.

• syntaxCount : Nat

  Expected number of arguments elaborator will process.

• argElaborators : ArgElaboratorArray self.syntaxCount
• resultScope : Option Nat
• argElabIndex : Array (Option Nat)

  Index into argElaborators for each argument (indexed by argLevel), None if arg has no syntax.

• preRegisterTypesScope : Option Nat

  If set, pre-register type names from children at this arg level before elaboration.

• preRegisterFunctionsScope : Option Nat

  If set, pre-register function signatures from children at this arg level before elaboration.

def StrataDDM.Elab.instInhabitedSyntaxElaborator.default : SyntaxElaborator

Equations

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

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedSyntaxElaborator : Inhabited SyntaxElaborator

Equations

• StrataDDM.Elab.instInhabitedSyntaxElaborator = { default := StrataDDM.Elab.instInhabitedSyntaxElaborator.default }

def StrataDDM.Elab.instReprSyntaxElaborator.repr : SyntaxElaborator → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance StrataDDM.Elab.instReprSyntaxElaborator : Repr SyntaxElaborator

Equations

• StrataDDM.Elab.instReprSyntaxElaborator = { reprPrec := StrataDDM.Elab.instReprSyntaxElaborator.repr }

@[reducible, inline]

abbrev StrataDDM.Elab.SyntaxElabMap : Type

Equations

• StrataDDM.Elab.SyntaxElabMap = Std.HashMap StrataDDM.QualifiedIdent StrataDDM.Elab.SyntaxElaborator

def StrataDDM.Elab.SyntaxElabMap.addDialect (m : SyntaxElabMap) (d : Dialect) : Except String SyntaxElabMap

Equations

• m.addDialect d = Array.foldlM (fun (x : StrataDDM.Elab.SyntaxElabMap) => StrataDDM.Elab.SyntaxElabMap.addDecl✝ x d.name) m d.declarations