Documentation

Mathlib.Lean.PrettyPrinter.Delaborator

Additions to the delaborator #

Assuming the current expression in a lambda or pi, descend into the body using an unused name generated from the binder's name. Provides d with both Syntax for the bound name as an identifier as well as the fresh fvar for the bound variable. See also Lean.PrettyPrinter.Delaborator.withBindingBodyUnusedName.

Equations
    Instances For

      Update OptionsPerPos at the given position, setting the key n to have the boolean value v.

      Equations
        Instances For

          Annotates stx with the go-to-def information of target.

          Equations
            Instances For

              Annotates stx with the go-to-def information of the notation used in stx.

              Equations
                Instances For