Hi Bill,
> Your NOTIN suggestion made great sense, but that's not the problem, it
> seems, because FunctionSpace/---> worked. I think HOL Light doesn't like
my
> weird infix -bb-->. HOL Light won't even take this as a function:
>
> let FunctionddSpace = new_definition
> `! s t. -dd--> s t = {f | (! x. x IN s ==> f x IN t) /\
> ! x. x NOTIN s ==> f x = @y. T}`;;
Yes, I missed that. The name "-dd-->" is irregular (it mixes symbolic and
alpha-numeric characters), and won't get parsed correctly in term quotations
in HOL Light. You have to construct terms involving "-dd-->" using the
syntax constructor functions (mk_comb, mk_eq, etc).
> How do you handle precedence in your HOL Zero? I'd guess it's similar
> to the way HOL Light does precedence.
I did a major review of HOL concrete syntax when designing HOL Zero, and
numerous details are handled differently from the other HOL systems.
Precedence is similar to HOL Light's, but type annotation generally requires
parentheses (although there are a few exceptions) - so `f a : A` in HOL
Light is `f (a:A)` in HOL Zero. Pairs are a special syntactic category,
where "," is a separator instead of being an infix operator, and outer
parentheses are mandatory - so `a,b,c` in HOL Light is `(a,b,c)` in HOL
Zero.
Mark.
------------------------------------------------------------------------------
LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial
Remotely access PCs and mobile devices and provide instant support
Improve your efficiency, and focus on delivering more value-add services
Discover what IT Professionals Know. Rescue delivers
http://p.sf.net/sfu/logmein_12329d2d
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
