Hi HOL4-user colleagues,
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.
Thanks
Flemming
Here is a dump of a few tests that I did last night:
hol4> hol
-----------------------------------------------------------------
HOL-4 [Kananaskis 4 (built Fri Jul 11 11:41:44 2008)]
For introductory HOL help, type: help "hol";
-----------------------------------------------------------------
[loading theories and proof tools ............. ]
[closing file "/home/fa/tools/HOL4/hol/tools/end-init-boss.sml"]
- val _ = new_theory"tp";
<<HOL message: Created theory "tp">>
- val tp1 = ==`:'a`==;
> val tp1 = ``:'a`` : hol_type
- ":tp1" = ":'a";
> val it = false : bool -- I expected this test to return true
- val p1 = (--`p1:tp1`--);
! Uncaught exception: -- Hmm, I thought that tp1 was a type
! HOL_ERR
- val tp2 = ==`:(tp1)list`==;
! Uncaught exception:
! HOL_ERR
- val tpx = ``:('a)list``;
> val tpx = ``:'a list`` : hol_type
- val x = --`x:^tpx`--; -- This used to work
! Toplevel input:
! val x = --[QUOTE " (*#loc 13 14*)x:", ANTIQUOTE (tpx),QUOTE " (*#loc 13
20*)"]--;
! ^^^
! Type clash: expression of type
! hol_type
! cannot have type
! term
- type_abbrev ("tp3", ``:'a``);
> val it = () : unit
- ":tp3" = ":'a"; -- So if tp3 is not a type abbreviation for
'a, what is it?
> val it = false : bool
- val p3 = (--`p3:tp3`--); -- what does the parser expect here?
Exception raised at Parse.parse_type:
on line 19, characters 17-19:
Insufficient arguments to abbreviated operator "tp3"
! Uncaught exception:
! HOL_ERR
-
-------------------------------------------------------------------------
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
