agda editor highlight

test.agda

{-# OPTIONS --type-in-type #-}
{- remark -}

module _ where

record Go (A : Set) : Set where
  constructor Go!
  field go : ∀ (a : A) → A → Set
  field og : A -> forall (a : A) -> Set
open Go {{...}} public

instance
  _ : Go Set
  _ = λ { .go X Y → X → Y ;
       .og X Y → Y → X }