On 2021-06-05 22:29, mechvel at scico.botik.ru wrote: > > agda $agdaLibOpt --guardedness +RTS -M24G -RTS Pol/Karatsuba.agda Note that you can put --guardedness in your project's .agda-lib file (if you have one): flags: --guardedness -- /NAD