[Agda] Inteligenta tipa kontrolilo?

[Martin Stone Davis]

I have difficulty reproducing the error. Using a recent version of Agda 
(from Apr 13) and using the latest master version of the 
standard-library, Agda reports this error:

code:
>   data _≤″_ (ω : Ω) : Ω → Set where
message:
> Multiple definitions of _≤″_. 

And when the end of this line is uncommented,
>   open import Data.Nat -- using (ℕ ; zero ; suc ; _+_ ; _<′_ ; fold)

Agda reports this error:

code:
>   incX-x,Sy : ∀ x y → incΩ x (x , suc y) ≡ zero , suc (y + x)
message:
> Could not parse the application
> incΩ x (x , suc y) ≡ zero , suc (y + x)




On 04/16/2016 03:34 PM, Serge Leblanc wrote:
> Estimata,
>
> Kial la tipa kontrolilo ne uzas mian antaŭan pruvon 'incX≡' por 
> unuaigi la tipon ⟨ incΩ (y + x) (suc″ (x , y)) ⟩ kun ⟨ suc x , y ⟩ ?
> Ĉu ekzistas metodo por fari tion?
> Why the type checker don't use my previous proof 'incX≡' for unify the 
> type ⟨incΩ (y + x) (suc "(x, y))⟩ with ⟨suc x, y⟩?
> Is there a method to do this?
>
> Sinceran antaŭan dankon.
> -- 
> Serge Leblanc
> ------------------------------------------------------------------------
> gpg --keyserver hkp://keyserver.ubuntu.com:11371 --recv-keys 0x67B17A3F
> Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160416/edd821d7/attachment-0001.html