[Agda] on `data' declaration

[Sergei Meshveliani]

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

[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

Post by Sergei Meshveliani
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.
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
https://lists.chalmers.se/mailman/listinfo/agda

[Sergei Meshveliani]

Great! Thank you.

--
SM

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
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.
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
https://lists.chalmers.se/mailman/listinfo/agda