[Agda] issue 779

[Serge D. Mechveliani]

Please, what may be a good work around for the bug No 779 ?

(Agda-2.3.2, MAlonzo).

I tried the construct of

  unity : LeftUnity S _*_
  unity = f 
          where         
          f : LeftUnity S _*_
          f  with mbU | hasUnity
          ... | leftUnity u | _ = u
          ... | unknown     | ()

in order to hide `with' inside
(see the code of my initial report).

And the report is different:

-----------------------------------------
Not a valid let-declaration
when scope checking
let mutual
      unity : LeftUnity S _*_
      unity = f
        where
          f : LeftUnity S _*_
          f with mbU | hasUnity
          ... | leftUnity u | _ = u
          ... | unknown | ()
in let mutual
         \epsilon : Setoid.Carrier S
         \epsilon = LeftUnity.\epsilon unity
   in let mutual
            _~~_ : _
            _~~_ = Setoid._~~_ S
      in (foo : \epsilon ~~ (\epsilon * \epsilon)) -> Set
-----------------------------------------

Thanks,

------
Sergei