This passes but shouldn't:
open import Agda.Builtin.Reflection
_ : Term
_ = quoteTerm {{x = Set}}
There is a check missing that the argument to quoteTerm is visible. (Such a check is in place for quote.)
As a general PL design principle, elaboration may not discard any information without comment: Either it is processed, or the user is warned that information will be discarded.
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