Andersen, Flemming L wrote: > I used to know how to use types and type abbreviations in HOL, but > either I have encountered a problem with this in my version of HOL4, > or I need some directions on how to use these features.
There are two facilities you can use to do this sort of thing, anti-quotation, and type_abbrev. Anti-quotation -------------- With anti-quotation, you make an ML level binding of a type, and then use that name inside types. As Wishnu said, you can write val tp1 = ``:'a`` val tp1_set = ``:^tp1 -> bool`` The complication with type anti-quotation is that if you want to anti-quote a type into a term, you have to use the magic ty_antiq function to get the types to work: val tm1 = ``x : ^(ty_antiq tp1)`` Of course, you can always set up an ML binding for the ty_antiq form: val tp1_t = ty_antiq ``:'a`` val tm1 = ``x : ^tp1_t`` See also the FAQ at http://hol.svn.sourceforge.net/viewvc/hol/HOL/doc/faq.html#Quotes Type abbreviations with type_abbrev ----------------------------------- With anti-quotation, the binding of name to type happened at the ML level. If you use type_abbrev, then you are setting up a map within the parser and printing facilities. For example: val _ = type_abbrev ("numset", ``:num -> bool``) Now, you can use numset as if it were a type: val derived_type = ``:int -> numset`` val derived_term = ``x : numset -> bool`` You can confirm the alias with - ``:num->bool`` = ``:numset``; > val it = true : bool If you try to set up an alias to something that includes type variables, then the name you specify becomes a type operator: val _ = type_abbrev("bag", ``:'a -> num``) val derived_type = ``:int bag`` val derived_term = ``f x : num bag`` If you do as you did, and try val _ = type_abbrev ("foo", ``:'a``) then you get an abbreviation that should behave like the identity type operator: - ``:'a foo`` > val it = ``:'a`` : hol_type - ``:'b foo`` > val it = ``:'b`` : hol_type Unfortunately, the code breaks on this degenerate case, and the pretty-printer loops when you try to print any non-variable type: - ``:bool`` > ... hangs ... ------------ One final thing: in your script, you started comparing types for equality by enclosing them in double quotes, e.g., "tp1" = "'a". This was sure to return false, because those values are strings, not types at all. Michael. ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
