Documentation

Lean.Widget.InteractiveGoal

Functionality related to tactic-mode and term-mode goals with embedded CodeWithInfos.

In the infoview, if multiple hypotheses h₁, h₂ have the same type α, they are rendered as h₁ h₂ : α. We call this a 'hypothesis bundle'. We use none instead of some false for booleans to save space in the json encoding.

  • names : Array String

    The user-friendly name for each hypothesis. Note that these are not Names: they are pretty-printed and do not remember the macro scopes.

  • fvarIds : Array Lean.FVarId

    The ids for each variable. Should have the same length as names.

  • The value, in the case the hypothesis is a let-binder.

  • isInstance? : Option Bool

    The hypothesis is a typeclass instance.

  • isType? : Option Bool

    The hypothesis is a type.

  • isInserted? : Option Bool

    If true, the hypothesis was not present on the previous tactic state. Only present in tactic-mode goals.

  • isRemoved? : Option Bool

    If true, the hypothesis will be removed in the next tactic state. Only present in tactic-mode goals.

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

    The shared parts of interactive term-mode and tactic-mode goals.

    Instances For

      An interactive tactic-mode goal.

      Instances For

        An interactive term-mode goal.

        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • g.pretty = g.pretty g.userName? g.goalPrefix
            Instances For
              Equations
              • g.pretty = g.pretty none "⊢ "
              Instances For

                Extend an array of hypothesis bundles with another bundle.

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

                    A variant of Meta.ppGoal which preserves subexpression information for interactivity.

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