[Agda] example with --sharing

[Ulf Norell]

A related problem was reported in issue 2235 (
https://github.com/agda/agda/issues/2235). Both
problems have been fixed (as of today).

/ Ulf

On Tue, Oct 4, 2016 at 1:49 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:

> I fail to link to "Report a bug", so I report here.
>
> This program is not type-checked by
>
>              agda $agdaLibOpts --sharing Foo.agda
>
> (in Development Agda of September16, 2016):
>
> ----------------------------------------------------------------------
> open import Relation.Binary  using (Setoid)
> open import Data.Maybe as Mb using (Maybe; just; nothing; Eq)
>
> module _ {α α=} {A : Setoid α α=}
>   where
>   open Setoid A using (_≈_) renaming (Carrier to C; refl to ≈refl)
>   open Setoid (Mb.setoid A) renaming (Carrier to C'; _≈_ to _='_)
>
>   fromMb : C → Maybe C → C
>   fromMb _ (just x) =  x
>   fromMb n nothing  =  n
>
>   cong-fromMb : {n n' : C} → {m m' : C'} → n ≈ n' → m =' m' →
>                                               fromMb n m ≈ fromMb n' m'
>
>   cong-fromMb {n} {n'} {m} {m'} n=n' m=m'  with  m | m' | m=m'
>   ...
>       | just _  | just _  | Mb.Eq.just x=y =  x=y
>   ... | nothing | nothing | _              =  n=n'
>   ... | nothing | just _  | ()
> ------------------------------------------------------------------------
>
>
> Regards,
>
> ------
> Sergei
>
> _______________________________________________
> 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/20161004/32a80753/attachment.html