[Agda] on `data' declaration

[Sergei Meshveliani]

Great! Thank you.

--
SM



On Tue, 2017-11-28 at 07:02 +0100, Ulf Norell wrote:
> 
> 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
> 
>