[Agda] `with' fail
Sergei Meshveliani
mechvel at botik.ru
Sat Apr 6 03:52:19 CEST 2019
People,
This is on Agda-2.6.0-candidate-II (ghc-8.6.3, Ubuntu Linux 18.04).
I try to replace `case` with `with' in
fr-noZeroDivisor : ¬ HasZeroDivisor frSemiring
fr-noZeroDivisor (f , (g , f≠0 , g≠0 , fg=0)) =
case
frNoZeroDiv {f} {g} fg=0
of \
{ (inj₁ f=0) → f≠0 f=0
; (inj₂ g=0) → g≠0 g=0
}
{-
with frNoZeroDiv {f} {g} fg=0
... | inj₁ f=0 = f≠0 f=0
... | inj₂ g=0 = g≠0 g=0
-}
`case' is type-checked fast.
And `with' type-checks for one minute, and then I interrupt it.
What can be the matter?
Regards,
------
Sergei
More information about the Agda
mailing list