[isabelle-dev] type unification

[Christian Sternagel]

Dear Dimitriy,

thanks that does the trick. However, after having a look at the 
implementation of Variable.polymorphic, I'm wondering whether it isn't 
overkill in my case. What about

   fastype_of #> Term.map_type_tfrees (TVar o apfst (rpair 0))

as alternative?

Since I'm manually "naming" schematic type variables apart before 
unification anyway, shouldn't that also work (without ever using a ctxt)?

cheers

chris

On 07/11/2013 02:57 PM, Dmitriy Traytel wrote:
> Hi Chris,
>
> I think Variable.polymorphic is what you want to use before using
> fastype_of.
>
> Dmitriy
>
> Am 11.07.2013 05:12, schrieb Christian Sternagel:
>> Dear list,
>>
>> what is the proper way of obtaining a type from a term, in case I want
>> to give it as argument to Sign.typ_unify (of Sign.typ_match for that
>> matter)?
>>
>> My question arises as follows. In adhoc_overloading.ML previously
>> Sign.the_const_type was used to obtain the type of a constant. The
>> result is a type with schematic type variables. Now that I want to use
>> terms instead of constants (as strings) I replaced Sign.the_const_type
>> by fastype_of, but this yields a type with fixed type variables and
>> thus unification may fail. So once again: What is the proper way of
>> getting a "schematic" type from a term?
>>
>> cheers
>>
>> chris
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>