[Agda] Re: problem using "with"

Nils Anders Danielsson nad at chalmers.se
Mon May 14 14:29:07 CEST 2012


On 2012-05-12 15:31, Wolfram Kahl wrote:
> Is there a way to view the generated with-function, with type declaration,
> especially in cases where it fails to type-check?

Use -vtc.with:20:

   {-# OPTIONS -vtc.with:20 #-}

   module Test where

   F : Set → Set
   F A with A
   ... | B = B

The debug printout includes the following:

   added with function .Test.with-3 of type Set → Set → Set -|

   buildWithClause returns .Test.with-3 A B = B

-- 
/NAD



More information about the Agda mailing list