Hi Bill, | I think it's quite interesting that HOL Light left out parentheses | val left_inv : thm = |- !x. elt_inv x prod x = unit
It is a tradition (which HOL Light inherits from lambda-calculus) that simple juxtaposition can be used for function application in the concrete syntax, i.e. just "f x" not necessarily "f(x)". Of course the parentheses may be needed if you have a composite expression for "x" in order to establish precedences. In particular, binary infix operators bind more loosely, so "f x + y" means "(f x) + y" not "f(x + y)". | This does not: *) | | parse_as_prefix "elt_inv";; | let left_inv = new_axiom | `!x . (inv x) prod x = unit`;; This is just the same problem isn't it, since you have "inv" not "elt_int"? It should work if you use the override_interface or overload_interface as recommended by Vincent, or use the name "elt_inv" explicitly. | Vincent, thanks for explaining that inv was already defined: | type_of `inv`;; | val it : hol_type = `:real->real` Yes indeed, thanks Vincent. | I'm an HOL Light newbie. What should I have read so that I would have | known that? Neither prefixes();; nor infixes();; lists `inv'. Well, all the manuals and all the source code, perhaps :-) It may be that this is not spelled out too clearly in the existing documentation, in fact, and I should say it more concretely. | Should I just make a habit of evaluating things like | type_of `elt_inv`;; | to see that I'm inventing a new type? The core question is whether something is already defined as a constant in the current state. Generally speaking, names in ` quotes ` that correspond to predefined constants are interpreted as those constants, and those that are not are interpreted as variables. (This is a slight simplification, because things are a bit different for bound variables.) There is no evident syntactic distinction between them, like the use of lower and upper case in Prolog. Note that the question of whether something parses as an infix, prefix or binder is largely orthogonal to whether it is a constant. The fact that the type is not completely general is a useful clue that something is a constant, though you can have constants with a completely general type (e.g. `@x. T`). More reliably, you can use "is_const": # is_const `inv`;; val it : bool = true # is_const `elt_inv`;; Warning: inventing type variables val it : bool = false You can get a list of all constants and their most general types with "constants()", but also be aware that the front-end names used in the parser may be different from the underlying constant names. The mapping is specified by the list "the_interface". It's via that mapping that the name "inv" is mapping to the underlying constant "real_inv" in your case and causing the problem. John. ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
