open public in record [Re: [Agda] reexport from record]

[Andreas Abel]

I was surprised by this behavior, but apparently you can only have an 
"open ... public" in a record if there aren't any more fields coming.

So, if you put field foo first, it should work.

Cheers,
Andresa

On 19.02.13 9:20 PM, Serge D. Mechveliani wrote:
> People,
> I have a strange behavior of a record export with `public'.
> The record is like this:
>
> -------------------------------------------------------------
> record Foo c l {upMon : UpMonoid c l} :  Set _
>    where
>    upMonoid = upMon
>    ...
>    setoid      = DecSetoid.setoid decSetoid
>    Carrier : Set c
>    Carrier = Setoid.Carrier setoid
>    _~_     = Setoid._\~~_ setoid       -- (math symbol replaced)
>
>    ~equiv : IsEquivalence {A = Carrier} _~_
>    ~equiv = Setoid.isEquivalence setoid
>
>    open IsEquivalence ~equiv public renaming
>                             (sym to ~sym; refl to ~refl; trans to ~trans)
>    field foo : Foo'
>    ...
> --------------------------------------------------------------
>
> I set `public' because the goal is to re-export  ~sym, ~refl, ~trans
> from Foo with renaming, in order to apply things like
>                                                        Foo.~sym r
>
> Another way to reexport it is to set   ~sym = IsEquivalence.sym ~equiv
>                                         ...
> instead of `open'.
> But for my code, the checker reports of "unsolved metas" - until I
> add signature for each of   ~sym, ~refl, ~trans.
> So, I have decided that  "open - public - renaming"  is shorter and
> nicer.
>
> Without `public', it is type checked, but  Б┬╪sym  is not exported.
> And inserting `public' leads to the report
> (in Agda-2.3.2 MAlonzo)
> ----------------------------------
> Not a valid let-declaration
> when scope checking
> let open
>        IsEquivalence ~equiv
>          public renaming (sym to ~sym; refl to ~refl; trans to ~trans)
> in (foo : Bool) -> Set
> -----------------------------------
>
> Is it an error in the checker?
> How to fix my program?
>
> The code fragment  with math symbols  is attached here as  t.agda.zip
>
> Thanks,
>
> ------
> Sergei
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/