open import Agda.Builtin.Unit open import Agda.Builtin.List open import Agda.Builtin.Reflection macro magic : Term → TC ⊤ magic hole = unify hole (pat-lam [] []) data ⊥ : Set where foo : ⊥ → ⊤ foo = magic -- __IMPOSSIBLE__ at Unquote.hs:513
The ExtLam constructor in Syntax.Reflected expects a non-empty list of clauses, but on the Agda side pat-lam takes any old list, so we have to handle the empty list case gracefully.
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