av :: module RsTQuotedDelim where data Bool : Set where true : Bool false : Bool dunno : Bool aa : {- :: -} Bool blip :: blop a : Bool a = bb