Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2015-11-01

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

All times shown according to UTC.

Time Nick Message
05:12 barrucadu joined #isabelle
17:56 tautologico why can't I use O (letter O) as a name?
18:03 ThreeOfEight because "O" is the predefined operator for composition of relations
18:03 ThreeOfEight it's an infix operator
18:03 ThreeOfEight as in "R O S"
18:03 ThreeOfEight …it is a bit confusing if you don't know about it
18:03 ThreeOfEight (same thing with small o, that's composition for functions. which is usually written as \<circ>)
18:07 tautologico I see
18:08 tautologico thanks
18:11 ThreeOfEight tautologico: you can delete this syntax using
18:11 ThreeOfEight no_notation relcomp (infixr "O" 75)
18:11 ThreeOfEight you probably shouldn't do that if you plan to have any of your code published in the Archive of Formal Proofs or something like that though
18:21 tautologico I can rename the variables, I was just curious why it happened
22:18 wagle joined #isabelle

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