[Agda] `let' in function signature
James Wood
james.wood.100 at strath.ac.uk
Sun Dec 24 21:06:02 CET 2017
Did you mean let q' = suc q, rather than suc n?
James
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
More information about the Agda
mailing list