I'm using agda-stdlib from this commit hash: https://github.com/agda/agda-stdlib/tree/97bc55e47367c562b3032bf104f2a00b19716f88 (version 2.1, not sure if it matters)
The following code causes Agda to run out of memory. I have 16 GB of RAM.
module Test where import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl) open Eq.≡-Reasoning using (begin_; step-≡-∣; step-≡-⟩; _∎) open import Data.Nat using (ℕ) easy : ∀ (m : ℕ) → m ≡ m easy m =begin -- <----------- this line m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ≡⟨⟩ m ∎
Note that there's no space between = and begin. If the space is added, it works as expected. If fewer m =<>s are supplied, it takes up quite a lot of memory but does terminate, showing an error starting with Cannot eliminate type m ≡ m with variable pattern =begin (did you supply too many arguments?) (which is probably correct).
Another example (original code where I ran into this problem):
module Test where import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; cong; sym) open Eq.≡-Reasoning using (begin_; step-≡-∣; step-≡-⟩; _∎) open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _^_) open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm) *-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p *-distrib-+ zero n p = refl *-distrib-+ (suc m) n p =begin -- <----------- this line (suc m + n) * p ≡⟨⟩ (suc (m + n)) * p ≡⟨⟩ p + (m + n) * p ≡⟨ cong (p +_) (*-distrib-+ m n p ) ⟩ p + (m * p + n * p) ≡⟨ sym (+-assoc p (m * p) (n * p)) ⟩ (p + m * p) + n * p ≡⟨⟩ suc m * p + n * p ∎
(Tested by saving this file as Test.agda and running agda Test.agda)
I'm on Fedora Linux 41, x86-64. Tested Agda versions: 2.7.0 (compiled from source), 2.7.0.1 (from github releases)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4