On 26/01/13 1:17 AM, hamed nemati wrote: > I would appreciate if someone could help me to find out how I can force > the Hol4 to print its output in a user defined format. For example, > using the following code snippet:
> type_abbrev("u8", ``:bool[8]``);
> val user_plus_def = Define `(user_plus (n:u8) (m:u8) =
> (n + m))`;
> EVAL``user_plus 2w 3w``;
> the output is :
>
> val it =
> |- bap_plus (2w :bool[8]) (3w :bool[8]) = (5w :bool[8])
> : Abbrev.thm
> I was wondering if there is way to get an output like:
>
> val it =
> |- bap_plus (2w :u8) (3w :u8) = (5w :u8])
> : Abbrev.thm
I assume you have show_types on (or, equivalently, have a set_trace
"types" 1).
In any case, I believe the intention is that you should get u8 displayed
when you do a type_abbrev like yours. So, I think this is a bug.
Thanks for the report. I’ve turned this into an tracked issue at
https://github.com/mn200/HOL/issues/106
Best,
Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS, MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft MVPs and experts. ON SALE this month only -- learn more at: http://p.sf.net/sfu/learnnow-d2d
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
