On 12/10/11 06:12, Jonathan von Schroeder wrote: > # real_neg;; > val it : thm = |- --x1 = mk_real (\u. ?x1. treal_neg x1 treal_eq u /\ > dest_real x1 x1)
> But I also don't really get why the rhs doesn't seem to "depend" on > x1 from the lhs since the x1 on the rhs is bound by the existential > quantification. There are two different x1 variables in the term, one of type real, and one of the type of the representation type for the reals. That means the conclusion of the theorem really is alpha-equivalent to your suggested rephrasing: > I would understand the theorem if it had the following form: > `--x1 = mk_real (\u. ?x2. treal_neg x2 treal_eq u /\ dest_real x1 x2)`;; The issue is that the pretty-printer creates a rather confusing string as its output; one that can't be parsed back into a term. On the other hand, the output really is a faithful representation of the underlying term. Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ All the data continuously generated in your IT infrastructure contains a definitive record of customers, application performance, security threats, fraudulent activity and more. Splunk takes this data and makes sense of it. Business sense. IT sense. Common sense. http://p.sf.net/sfu/splunk-d2d-oct
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
