Derivation of EvalConfigItem

This module defines defEvalConfigItem, which derives an EvalConfigItem object for structures. Its main interface are the command syntaxes defined in Lean.Elab.ConfigEval.Commands.

inductive Lean.Elab.ConfigEval.EvalConfigItemHandlerKind : Type

• exact : EvalConfigItemHandlerKind

  Handler is called when its key matches the configuration key exactly. The matched key is not allowed to be Name.anonymous.

• wildcard : EvalConfigItemHandlerKind

  Handler is called when its key is a strict prefix of the configuration key. The matched key may be Name.anonymous.

def Lean.Elab.ConfigEval.instBEqEvalConfigItemHandlerKind.beq : EvalConfigItemHandlerKind → EvalConfigItemHandlerKind → Bool

Equations

• Lean.Elab.ConfigEval.instBEqEvalConfigItemHandlerKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Lean.Elab.ConfigEval.instBEqEvalConfigItemHandlerKind : BEq EvalConfigItemHandlerKind

Equations

• Lean.Elab.ConfigEval.instBEqEvalConfigItemHandlerKind = { beq := Lean.Elab.ConfigEval.instBEqEvalConfigItemHandlerKind.beq }

structure Lean.Elab.ConfigEval.EvalConfigItemHandler : Type

• ref : Syntax

  Ref for the key.

• key : Name

  The key that's handled. May be anonymous for certain kinds.

• kind : EvalConfigItemHandlerKind

  The kind of match this handler is looking for.

• body : Term

  A function fun cfg item => ....

• projFn? : Option Name

  Constant to use for terminfo. This is added to the HandlerTrie.

• struct? : Option Name

  Constant to use for field completion terminfo.

structure Lean.Elab.ConfigEval.EvalConfigItemView : Type

• omitFields : Array (Ident × Name)

  Fields to not automatically synthesize handlers for, in addition to those keys already appearing in handlers.

• handlers : Array EvalConfigItemHandler

  Explicitly provided handlers.

def Lean.Elab.ConfigEval.evalBoolItem (item : ConfigItem) : TermElabM Bool

Precompiled version of evalTermOrExprWithElab (α := Bool) that also makes use of the cached item.bool? value.

Equations

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

def Lean.Elab.ConfigEval.addConstInfo' (ref : Syntax) (projFn : Name) : TermElabM Unit

Equations

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

def Lean.Elab.ConfigEval.defEvalConfigItem (doc? : Option (TSyntax `Lean.Parser.Command.docComment)) (vis? : Option (TSyntax `Lean.Parser.Command.visibility)) (kind : TSyntax `Lean.Parser.Term.attrKind) (tk : Syntax) (struct fnIdent : Ident) (extraBinders : TSyntaxArray `Lean.Parser.Term.bracketedBinder) (view : EvalConfigItemView) : Command.CommandElabM Unit

Makes an EvalConfigItem for the structure. Supports structures with no parameters or universes.

Equations

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