[Agda] type checking in real-world algebra

[Nils Anders Danielsson]

On 2020-01-27 22:57, mechvel at scico.botik.ru wrote:
> I have the two observations on this.
> 
> (I) Substituting the instances of generic structures (Group, Ring ...)
>      for ℤ, Fraction ℤ, Pol (Fraction ℤ) and trying to type-check there
>      a simple function often leads to the performance problem in the
>      type check.
> (II) In such cases, using `with' aggravates this problem greatly.
>       It is better to introduce a function instead.
> 
> What people, please, think of this?

https://agda.readthedocs.io/en/v2.6.0.1/language/with-abstraction.html#performance-considerations

-- 
/NAD