[Agda] boundings in data-where
Serge D. Mechveliani
mechvel at botik.ru
Mon Nov 5 21:07:22 CET 2012
People,
there is a strange syntax difference between the `record' and `data'
declarations with respect to bounding and `open' after `where'.
Consider the example:
------------------------------------------------------------------------
record LeftQuotient {c l : Level} (H : Semigroup c l)
(a b : Semigroup.Carrier H) : Set (max c l)
where
open Semigroup {{...}} -- (1)
_~_ = Semigroup._\~~_ H -- (2)
field
quot : Semigroup.Carrier H
...
data MbDivideLeft {c l : Level} (H : Semigroup c l)
(a : Semigroup.Carrier H) (b : Semigroup.Carrier H) : Set (max c l)
where
open Semigroup {{...}} -- (1')
_~_ = Semigroup._\~~_ H -- (2')
...
unsolvable :
(x : Carrier H) -> \neg ((x * b) ~ a) -> MbDivideLeft H a b
...
------------------------------------------------------------------------
The lines (1) and (2) do work, while (1') and (2') do not parse.
Has it sense to make this feature in `data' similar as in 'record' ?
Thanks,
Sergei.
More information about the Agda
mailing list