[Agda] `let' in function signature
Sergei Meshveliani
mechvel at botik.ru
Sun Dec 24 22:17:29 CET 2017
Yes, thank you.
Please, withdraw my request
------
Sergei
On Sun, 2017-12-24 at 20:06 +0000, James Wood wrote:
> Did you mean let q' = suc q, rather than suc n?
Yes, thank you.
Please, withdraw my request. Sorry for noise.
------
Sergei
> On 24/12/17 19:58, Sergei Meshveliani wrote:
> > 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
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
More information about the Agda
mailing list