> This is not possible: you cannot define a function that accesses the > syntax of terms *in the logic*. Every function in the logic respects > Leibniz's law, i.e., x = y implies f x = f y (where = is logical > equality). Ok, thank you for this clarification.
> If you want to reason about the syntax of terms in the logic, you will > need a deep embedding of your terms, i.e., you need to define a > (recursive) data type (in the logic) that models the syntax. You will > probably also want to define the semantics of terms (as a function on > this data type). > > Hope this helps! It does, thank you very much :-) best Rasmus ------------------------------------------------------------------------------ Start uncovering the many advantages of virtual appliances and start using them to simplify application deployment and accelerate your shift to cloud computing. http://p.sf.net/sfu/novell-sfdev2dev _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
