[Agda] on `data' declaration

[Ulf Norell]

module _ (c x y d : ℕ) where
  private e = c + (y * y + y)
  data Foo : Set where
    foo1 : x < e → Foo
    foo2 : x > e → (x ≡ e + d) → Foo

/ Ulf

On Mon, Nov 27, 2017 at 8:24 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> People,
>
> consider the declaration like
>
>  data Foo (c x y d : ℕ) :  Set
>       where
>       let e = c + (y * y + y)
>
>       foo1 : x < e → Foo c x y d
>       foo2 : x > e → (x ≡ e + d) → Foo c x y d
>       foo3 : ...
>
>
> Agda rejects it. And the programmer is forced to set several times the
> expanded expression for  e  in several data constructors.
>
> I wrote
>
>  private expr =  \c y ->  c + (y * y + y)
>
>  data Foo (c x y d : ℕ) :  Set
>       where
>       foo1 : x < expr c y → Foo c x y d
>       foo2 : x > expr c y → (x ≡ (expr c y) + d) → Foo c x y d
>       foo3 : ...
>
> Can anybody, please, suggest any better way out?
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20171128/0d2ae839/attachment.html>