[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