[Agda] reasoning combinator names

[Sergei Meshveliani]

On Tue, 2019-05-28 at 09:09 +0100, Guillaume Allais wrote:
> Hi Sergei,
> 
> What we usually do in the standard library is to only open the module
> for equational reasoning locally to the definition which needs it.
> This way users can quickly see which reasoning toolkit is being used.
> 
> You can see this in action in e.g. Data.Integer.DivMod where we have
> both:
> 
> =====================================================================
> foo m n p = begin
>   (...)
>  ∎ where open ≤-Reasoning
> =====================================================================
> 
> and
> 
> =====================================================================
> bar x y = begin
>   (...)
>  ∎ where open ≡-Reasoning
> =====================================================================


Thank you!
I have forgotten of this possibility.

------
Sergei 



> --
> gallais
> 
> On 27/05/2019 19:24, Sergei Meshveliani wrote:
> > People,
> > 
> > I have  Foo.agda  where it is needed reasoning by combinators of
> > standard-library-master for _≡_ and _≤_ for different types, as follows.
> >  
> > * reasoning with _≡_ on ℕ and FooData,  
> > * reasoning with _≤_ on ℕ.  
> > 
> > I usually agree such reasonings by renaming some of the reasoning
> > combinators.
> > But this time such renaming is forbidden. 
> > What reasoning modules to import, what to substitute?
> > 
> > Thanks,
> > 
> > ------
> > Sergei
> > 
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> > 
>