{-# OPTIONS --cohesion --erasure #-}
import Agda.Builtin.Bool
postulate
Flat : (@♭ A : Set) → Set
module @0 Bool where
open module M (@♭ A) (_ : Flat A) = Agda.Builtin.Bool public
This prints the module abstraction as module M @♭ A (_ : Flat A), which does not parse because of missing parenthesis around @♭ A.
Found this bug by reading the code for the printer:
instance Pretty NamedBinding where pretty (NamedBinding withH x) = prH $ if | Just l <- isLabeled x -> text l <+> "=" <+> pretty xb | otherwise -> pretty xb where xb = namedArg x bn = binderName xb prH | withH = prettyRelevance x . prettyHiding x mparens . prettyCohesion x . prettyQuantity x . prettyTactic bn | otherwise = id -- Parentheses are needed when an attribute @... is present mparens | noUserQuantity x, Nothing <- bnameTactic bn = id | otherwise = parensThis code bit-rotted when cohesion was added in
4a45eb9; the
noUserQuantity
check became insufficient to check whether there are modalities.
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