Hi all,
im currently having a problem figuring out the meaning of the following
theorem (from realax.ml):
# real_neg;;
> val it : thm =
> |- --x1 = mk_real (\u. ?x1. treal_neg x1 treal_eq u /\ dest_real x1 x1)
What puzzles me mostly is the fact, that neither I nor HolLight can figure
out a correct typing for x1:
# `--x1 = mk_real (\u. ?x1. treal_neg x1 treal_eq u /\ dest_real x1 x1)`;;
> Exception: Failure "typechecking error (initial type assignment)".
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.
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)`;;
Because then we'd build the equivalence class of all negatives of
hreal*hreal's that are in the equivalence class x1 (if we take real to be
the set of equivalence classes of hreal*hreal as specified by the quotient
type).
I'd greatly appreciate and information or suggestions that can shed light on
my issue end point me to any misconceptions I might have.
Jonathan
------------------------------------------------------------------------------
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
