I accidentally wrote List T instead of List T -> List T earlier today, which led to a failure in the pretty printer. This appears to be a bug.
MWE:
module test where data ⊤ : Set where tt : ⊤ data List (A : Set) : Set where [] : List A _∷_ : A → List A → List A _ : List ⊤ _ = tt ∷_
output:
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at
src/full/Agda/Syntax/Concrete/Pretty.hs:239:17 in
Agda-2.8.0-8a21JzGgARL9KK0zE4Xa4q:Agda.Syntax.Concrete.Pretty
Agda version: built from master.
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