[Ur] disjointness proof in type-level functions

[Adam Chlipala]

On 08/07/2013 12:04 PM, Sergey Mironov wrote:
> 2013/8/7 Sergey Mironov<grrwlf at gmail.com>:
>    
>>> Also, have you considered just referring to users by name to simplify your
>>> schema?
>>>        
>> Yes, but seems I need generic case in my app: users should be able to
>> register themselves. I'll need user roles as well, and that is what
>> I'll refer to by name.
>>      
> Ah, Or did you mean using plain
>
> table users : {Name : string, Pass : string} PRIMARY KEY Id
>
> instead of constructors?
>    

Yes, that's what I meant.

> By the way. Need syntax hint. Can I translate 'fun .. and' syntax into 'val's ?
>
> For example,
>
> fun loginHandler row = ..
> and login {} = ...
>
> into
>
> val loginHandler : $(login_form) ->  transaction page = fn li =>
> and login : unit ->  transaction page = fn {} =>  ...
>
> (does not work as written because of syntax errors reported by the compiler)
>    

You just need to add [rec] after [val].