You are right. Thanks for the clarification! - chris
On 07/11/2013 04:19 PM, Dmitriy Traytel wrote:
If you are planing to localize the thing, you'll have to take the
context into account. I guess you don't want to generalize over fixed
type variables (as your solution does).
locale A =
fixes a :: 'a
begin
ML {*
val T1 = @{term a} |> singleton (Variable.polymorphic @{context}) |>
fastype_of
val T2 = @{term a} |> (fastype_of #> Term.map_type_tfree (TVar o
apfst (rpair 0)))
*}
end
Dmitriy
Am 11.07.2013 09:01, schrieb 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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
