Consider:
module Test19 where
open import Agda.Builtin.String
open import Agda.Builtin.Nat
postulate
show : ∀ {ℓ} {A : Set ℓ} → A → String
_ = {! 123 !}
Hitting C-u enough times (so Agda will use the show function) results in the error message Not a string: show 123. When the show function reduces, it's even harder to know what's gone wrong. This error message should mention that we were trying to use a show instance for printing.
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