Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-03-03

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

All times shown according to UTC.

Time Nick Message
02:23 lispy joined #isabelle
03:25 int-e_ joined #isabelle
05:40 JCaesar I had a proof(rule,rule,rule,rule,rule,rule refl,rule,rule refl,rule,rule refl,rule refl). Now I have flex-pairs. *deletes entire file and starts anew*
06:51 ThreeOfEight JCaesar: did you get any further with your stuff?
06:53 JCaesar I tried a bit in the morning, but no… OpenFlow is higher on the list anyway.
06:55 ThreeOfEight If you give me access to your entire code, I can take a shot at it, if you want.
06:58 JCaesar If you want to waste your time on it… I don't need that for anything at the moment, I just think that it would be a very nice addition to the bdds we made…
07:16 ThreeOfEight I would like to take a look at it, yes.
07:17 ThreeOfEight What is it for exactly anyway?
09:22 JCaesar ThreeOfEight: You should have just received an email from github…
09:22 JCaesar for exactly… nothing yet.
09:23 JCaesar the idea is that if you represent the set of packets accepted by a bdd where the variables correspond to the bits in the header, then you can't do much with that representation in the current state of the bdd package.
09:23 JCaesar yes, you can test whether they're equal, that's nice, but not all that helpful.
09:24 JCaesar Especially, you might want to obtain a firewall back that is equivalent to what is represented by the bdd.
09:30 JCaesar That way you're even going to get a firewall that only consists of accepts and a single deny all at the end (or the other way around). Which might be nice if we're going to attempt to rewrite stateful firewalls to stateless firewalls.
10:10 ThreeOfEight okay
10:14 chuchucorny joined #isabelle
10:16 ThreeOfEight JCaesar: fyi, a lot of your functions can be defined with "primrec" instead of "fun"
10:16 ThreeOfEight the advantage is that primrec is faster and more light-weight
10:16 ThreeOfEight if you need the elim rules that fun generates or something like that, you can still use fun, but otherwise I'd use primrec
10:16 ThreeOfEight because when you use fun where primrec would suffice, you get a tonne of lemmas you don't need
20:00 dmiles joined #isabelle

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