On Sun, Oct 31, 2010 at 3:35 PM, Sylvain Le Gall <sylvain@le-gall.net> wrote:
> On 31-10-2010, Wojciech Daniel Meyer <wojciech.meyer@googlemail.com> wrote:
>> bluestorm <bluestorm.dylc@gmail.com> writes:
>>
>>> It was actually the case in Caml Light : each datatype constructor
>>> implicitly declared a constructor function with the same name. I
>>> don't exactly know why this feature was dropped in Objective Caml,
>>> but I think I remember (from a previous discussion) that people
>>> weren't sure it was worth the additional complexity.
>>
>> Would that be not possible now with Camlp4 extension?
>>
>
> I am pretty sure, it is possible to implement them with camlp4. Just a
> matter of time -- and motivation.
>
> The only limitation I can see, is that the generated constructors won't
> be capitalized. E.g.:
>
> type t = MyConstr | YourConstr of int
>
> =>
>
> type t = MyConstr | YourConstr of int
>
> let myConstr = MyConstr
> let yourConstr i = YouConstr i
>

Why do you say so? HOL Light uses capitalized identifiers for values,
for example. It's probably possible to do whatever one reasonably
wants.