def ProofWidgets.CheckHighlight (name : Lean.Name) (showAlt : Bool) : Lean.MetaM Unit

Print the signature of name as a widget message in the infoview with dimmed implicit arguments (opacity 50%).

Arguments:

• name: fully qualified name of the constant to print the signature of
• showAlt: if false, implicit arguments are omitted from the alt argument of MessageData.ofWidget

Equations

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

def «command#checkh_» : Lean.ParserDescr

A version of #check that dims implicit arguments in the infoview, and omits them completely in non-interactive output (e.g. on the command-line).

Equations

• «command#checkh_» = Lean.ParserDescr.node `«command#checkh_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#checkh ") (Lean.ParserDescr.const `ident))

def «command#checkh'_» : Lean.ParserDescr

A version of #check that dims implicit arguments in the infoview, and displays them as usual in non-interactive output (e.g. on the command-line). See also #checkh.

Equations

• «command#checkh'_» = Lean.ParserDescr.node `«command#checkh'_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#checkh' ") (Lean.ParserDescr.const `ident))