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.

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
      • The name foo in case foo, if any.

        userName? : Option String
      • The symbol to display before the target type. Usually ⊢ ⊢ but conv goals use ∣ ∣ and it could be extended.

        goalPrefix : String
      • Identifies the goal (ie with the unique name of the MVar that it is a goal for.)

        mvarId : Lean.MVarId
      • If true, the goal was not present on the previous tactic state.

        isInserted? : Option Bool
      • If true, the goal will be removed on the next tactic state.

        isRemoved? : Option Bool

      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.

          Extend an array of hypothesis bundles with another bundle.

          Equations
          • One or more equations did not get rendered due to their size.
          def Lean.Widget.withGoalCtx {n : TypeType} [inst : MonadControlT Lean.MetaM n] [inst : Monad n] [inst : Lean.MonadError n] [inst : Lean.MonadOptions n] [inst : Lean.MonadMCtx n] {α : Type} (goal : Lean.MVarId) (action : Lean.LocalContextLean.MetavarDecln α) :
          n α
          Equations
          • One or more equations did not get rendered due to their size.

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

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