[Agda] +-mono arguments

[Andrés Sicard-Ramírez]

Please attach a MCV (minimal, complete and verifiable) example.

On 22 March 2015 at 07:39, Sergei Meshveliani <mechvel at botik.ru> wrote:
> Who knows, please,
> is it possible to cancel below explicit signatures for  1≤sm  and  sm≤sm
> and to use their values directly as arguments for  _+-mono_
> ?
>
> (see attachment)
>
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>



-- 
Andrés