Camelia, the Perl 6 bug

IRC log for #isabelle, 2013-02-17

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
14:54 kaki joined #isabelle
15:01 kaki Hello! I'm trying to formalize the following definition in Isabelle: We call S a line segment iff there is a P \subset \mathbb{R}^2 such that |P| = 2 and S = {p*t+(1-t)*q  | t\in[0,1] and p,q \in P}
15:05 kaki I tried it with definition LineSegment :: "'a \<Rightarrow> bool" where "LineSegment S = (\<exists>P::(real*real) set. card P = 2 \<and> S = {x::(real*real). x = p*(t::real)+(1-t)*q \<and> 0\<le>t \<and> t\<le>1 \<and> p\<in>P \<and> q\<in>P})"
15:05 kaki And Isabelle isn't accepting this Definition because of failing to meet type constraint
15:06 kaki I imported Complex_Main and did nothing else than this definition in this theory
15:09 kaki another question is, what package to import to have isabelle understand things like value "(3::real,2::real)*3::real"
15:09 kaki that means, vector calculations, scalar multiplications
16:46 mekeor joined #isabelle

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary