open import Agda.Builtin.Nat
variable x : Nat
{-# BUILTIN NATPLUS x #-}
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at
src/full/Agda/TypeChecking/Rules/Application.hs:376:26 in
Agda-2.8.0-Jy3QZyfEPpVKHSr0q4RiRx:Agda.TypeChecking.Rules.Application
Observed when trying to find reproducers for more unusual error messages.
On Agda master branch 8dfe79a.
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