[Ur] disjointness proof in type-level functions

[Adam Chlipala]

On 08/07/2013 10:46 AM, Sergey Mironov wrote:
> Hi. I faced a problem while exploring the type system. Looks like I
> can't define a constructor-level function which adds a field (of int
> type) to the record.

You're right that there is no disjointness obligation kind like the 
disjointness obligation type.  There isn't a general way to do the sort 
of abstraction you've asked about.  However...

> I need this to teach
> my app to define tables for custom records, adding primary key named
> Id, like
>
> con c_users = [ Name = string, Pass = string]
>
> ..
>
> table users : $(addIntField #Id c_users) PRIMARY KEY Id
>    

Isn't it actually fewer characters to write
     [Id = int] ++ c_users
instead, while also saving others who read your code from having to 
learn a new defined function?

Also, have you considered just referring to users by name to simplify 
your schema?