This is idle curiosity on my part about HOL Light: why are the constants that
support set comprehensions defined in such a way that the parser has to
generate an invisible bound variable? This results in surprising behaviour like:
# `{x | x > 9}` = `{x | x > 9}`;;
val it : bool = false
HOL4 defines set comprehensions the way I would expect (using a single constant
GSPEC with type 'a -> 'b # BOOL -> 'b -> BOOL) and doesn't need to insert any
invisible bound variables.
Regards,
Rob.
------------------------------------------------------------------------------
Shape the Mobile Experience: Free Subscription
Software experts and developers: Be at the forefront of tech innovation.
Intel(R) Software Adrenaline delivers strategic insight and game-changing
conversations that shape the rapidly evolving mobile landscape. Sign up now.
http://pubads.g.doubleclick.net/gampad/clk?id=63431311&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
