[Agda] reasoning combinator names

[Guillaume Allais]

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
=====================================================================

Best,
--
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
>