Issue1137.agda:10,1-14,10
Termination pragmas are ignored in where clauses
(see https://github.com/agda/agda/issues/3355)
when scope checking the declaration
  foo = bar
    where
      {-# TERMINATING #-}
      bar : A
      bar = a

———— All done; warnings encountered ————————————————————————

Issue1137.agda:10,1-14,10
Termination pragmas are ignored in where clauses
(see https://github.com/agda/agda/issues/3355)
when scope checking the declaration
  foo = bar
    where
      {-# TERMINATING #-}
      bar : A
      bar = a
