Agda-2.3.2.2: test/interaction/RecordUpdateSyntax.agda

module RecordUpdateSyntax where

data ⊤ : Set where
  tt : ⊤

record R : Set where
  field
    a b : ⊤

test : R
test = record {!!} { a = tt }