When an underscore is created during expansion of pattern synonyms, it lacks the scope info.
The symptom is that constraints are printed in top-level scope (with lots of qualification).
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
data D : Set where
c : { i : true ≡ false } → D
pattern ff {i} = c {i}
works : D
works = c
-- yellow:
-- _i_6 : true ≡ false
test : D
test = ff
-- yellow:
-- _i_8
-- : Agda.Builtin.Bool.Bool.true Agda.Builtin.Equality.≡
-- Agda.Builtin.Bool.Bool.false
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