[Agda] Re: problem using "with"

[Nils Anders Danielsson]

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