The following code triggers an internal error:
open import Agda.Builtin.Equality f : (A : Set) → refl ≡ refl f A with f _ … = ?
An internal error has occurred. Please report this as a bug.
Location of the error: impossible, called at
src/full/Agda/TypeChecking/Rules/LHS.hs:742:95 in
Agda-2.8.0-7D9KvK7GwQkHp5q0eLV7UR:Agda.TypeChecking.Rules.LHS
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