[Ur] introducing a name in functor body

Adam Chlipala adamc at impredicative.com
Thu Dec 1 09:22:20 EST 2011


Gergely Buday wrote:
>> The problem is the same as if you had merely written [val foo : int] instead
>> of [val foo = 3]: you are writing an _interface_ declaration (i.e.,
>> "signature item") in a position that expects an _implementation_ declaration
>> (just called "declaration" in the manual).  There is no declaration for
>> generating a fresh name automatically; you would probably take that name
>> into the functor as an input.
>>      
> But this is a field name that I want to use independently of an input
> structure. I put it outside the functor but in vain. How can I declare
> this field name to be used later?
>    

I don't understand the question.  As I said, the full set of constant 
field names exists in every context without declaration.



More information about the Ur mailing list