Discussion:
`let' in function signature
(too old to reply)
Sergei Meshveliani
2017-12-24 19:58:43 UTC
Permalink
Raw Message
Please, what is wrong in the below program?

---------------------------------------------------------------
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Data.Nat using (ℕ; suc; pred; _*_; _^_)

postulate anything : ∀ {a} {A : Set a} → A
postulate pSum : ℕ → ℕ → ℕ

pSum-eq : (q n : ℕ) → let q' = suc n
in
(pSum q' n) * q ≡ pred (q' ^ (suc n)) -- (1)
pSum-eq 1 0 = goal
where
postulate goal : (pSum 2 0) * 1 ≡ pred (2 ^ 1)

pSum-eq _ _ = anything
----------------------------------------------------------------

Agda 2.5.3 reports

2 != 1 of type ℕ
when checking that the expression goal has type
pSum 1 ℕ.zero * 1 ≡ pred (1 ^ 1)

After replacing q' with (suc q) in the line (1), the type check
succeeds.

Is this a bug?

Regards,

------
Sergei
James Wood
2017-12-24 20:06:02 UTC
Permalink
Raw Message
Did you mean let q' = suc q, rather than suc n?

James
Post by Sergei Meshveliani
Please, what is wrong in the below program?
---------------------------------------------------------------
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Data.Nat using (ℕ; suc; pred; _*_; _^_)
postulate anything : ∀ {a} {A : Set a} → A
postulate pSum : ℕ → ℕ → ℕ
pSum-eq : (q n : ℕ) → let q' = suc n
in
(pSum q' n) * q ≡ pred (q' ^ (suc n)) -- (1)
pSum-eq 1 0 = goal
where
postulate goal : (pSum 2 0) * 1 ≡ pred (2 ^ 1)
pSum-eq _ _ = anything
----------------------------------------------------------------
Agda 2.5.3 reports
2 != 1 of type ℕ
when checking that the expression goal has type
pSum 1 ℕ.zero * 1 ≡ pred (1 ^ 1)
After replacing q' with (suc q) in the line (1), the type check
succeeds.
Is this a bug?
Regards,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Sergei Meshveliani
2017-12-24 21:17:29 UTC
Permalink
Raw Message
Yes, thank you.

Please, withdraw my request

------
Sergei
Post by James Wood
Did you mean let q' = suc q, rather than suc n?
Yes, thank you.

Please, withdraw my request. Sorry for noise.

------
Sergei
Post by James Wood
Post by Sergei Meshveliani
Please, what is wrong in the below program?
---------------------------------------------------------------
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Data.Nat using (ℕ; suc; pred; _*_; _^_)
postulate anything : ∀ {a} {A : Set a} → A
postulate pSum : ℕ → ℕ → ℕ
pSum-eq : (q n : ℕ) → let q' = suc n
in
(pSum q' n) * q ≡ pred (q' ^ (suc n)) -- (1)
pSum-eq 1 0 = goal
where
postulate goal : (pSum 2 0) * 1 ≡ pred (2 ^ 1)
pSum-eq _ _ = anything
----------------------------------------------------------------
Agda 2.5.3 reports
2 != 1 of type ℕ
when checking that the expression goal has type
pSum 1 ℕ.zero * 1 ≡ pred (1 ^ 1)
After replacing q' with (suc q) in the line (1), the type check
succeeds.
Is this a bug?
Regards,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Loading...