Missing-field hints for structure instance elaborator #
This module generates suggested edits for structure instance notation that is missing required fields. The suggestions adapt to the style of the existing structure instance syntax and automatically insert any values inferred via constraints generated by already present fields.
def
Lean.Elab.Term.StructInst.mkMissingFieldsHint
(fields : Array (Name × Option Expr))
(stx : Syntax)
:
Creates a hint message for the "fields missing" error that fills in the missing fields, adapting to the structure instance notation style of the current syntax. Note that if the syntax is malformed or synthetic, this function returns an empty message instead.
Equations
- One or more equations did not get rendered due to their size.