{- Globular types as a coinductive record -}
record Glob : Set1 where
coinductive
field
Ob : Set
Hom : (a b : Ob) → Glob
open Glob public
record Unit : Set where
{- The terminal globular type -}
Unit-glob : Glob
Ob Unit-glob = Unit
Hom Unit-glob a _ = Unit-glob
The previous module fails with the following error
Not implemented: copatterns with patterns before the principal
argument
when scope checking the declaration
mutual
Ob Unit-glob = Unit
Hom Unit-glob a _ = Unit-glob
From guillaum...@gmail.com on September 18, 2013 16:32:15
{-# OPTIONS --copatterns #-}
module Test where
{- Globular types as a coinductive record -} record Glob : Set1 where coinductive field Ob : Set Hom : (a b : Ob) → Glob open Glob public
record Unit : Set where
{- The terminal globular type -} Unit-glob : Glob Ob Unit-glob = Unit Hom Unit-glob a _ = Unit-glob
The previous module fails with the following error
Not implemented: copatterns with patterns before the principal argument when scope checking the declaration mutual Ob Unit-glob = Unit Hom Unit-glob a _ = Unit-glob
Changing the underscore to a dummy name works.
Original issue: http://code.google.com/p/agda/issues/detail?id=905