Skip to content

Infinite goals added upon reload! #264

@kontheocharis

Description

@kontheocharis

Version: 0.7.8 (pre-release)

Sometimes, especially in large files with some goals, when I add a new goal and reload, the language server just keeps adding goals and I have to force quit VSCode to stop it. Not sure if it is a problem with the language server itself or agda-mode-vscode.

   ∣elim-Nat-ω∣ : ∀ {X~ : (p : $) → Tm z Nat → Ty}
        → {mz~ : (p : $) → Tm ω (X~ p [ zero {ω} ])}
        → {ms~ : (p : $) → (n : Tm ω Nat) → Tm ω (X~ p [ n ]) → Tm ω (X~ p [ succ n ])}
        → {n~ : (p : $) → Tm ω Nat}
        → ∣ (λ p → elim-Nat (X~ p) (mz~ p) (ms~ p) (n~ p)) ∣
            ≡ rec ∣ mz~ ∣ ((λ a b →{!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}!   !}{!  {!   !}!})) {!   !}

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions