[Agda] type check performance

[Wolfram Kahl]

On Thu, Jan 12, 2017 at 09:35:26PM +0300, Sergei Meshveliani wrote:
> On Wed, 2017-01-11 at 14:21 -0500, Wolfram Kahl wrote:
> > Can you go to the top-level of the file module in which this is defined,
> > and ask for the type  (C-c C-d) of the qualified name of remByDivisor,
> > qualified as necessary to be able to refer to it from the top-level
> > of the file module?
> > 
> > And also do that for each of  ∣  ,  eucRem ,  ≈ , and  0# ?
> > 
> > If my understanding is correct, then at least in some circumstances
> > and to a certain degree, these are the types that Agda is really dealing with.
> > 
> 
> I have there
> 
> --------------------------------------------
> open import Level using (_⊔_)
> ...
> ...
> module OfEuclideanRing {α α=} (upIR∣? : UpIntegralRing-with∣? α α=)
>                  (open OverIntegralRing-0 upIR∣? using (EuclideanRing))
>                  E : EuclideanRing)  
>   where
>
> [...]
> 
>   remByDivisor : (a b : C) → b ∣ a → eucRem a b ≈ 0#
>   ...
> --------------------------------------------               
> 
> I go to the beginning of this file and command
> 
>   C-c C-d  
>   remByDivisor
> 
> And it prints its type.

I just tried something like that myself, and apparently my instructions
were no good --- sorry! Better create a test file:

Test1.agda:

 | module Test1 where
 | 
 | import OfEuclideanRing

and then do

  C-c C-d OfEuclideanRing.remByDivisor

there.


Wolfram