I was using the following Singleton datatype for tests and by force of habit made the mistake of calling agsy on the hole for the singleton corresponding to a large natural number. Needless to say, I had to prompty kill emacs. And clean up my file now mostly filled with suc(k)s.
I'd argue that any term with depth > 10 is probably not worth printing. A principled solution would be to make it possible to override this default by passing an option in the goal as is already the case for e.g. allowing it to do case-splitting.
open import Agda.Builtin.Nat
data Singleton {A : Set} : A → Set where
_! : (a : A) → Singleton a
_ : Singleton 1005
_ = ? -- don't call agsy here
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