Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2015-12-15

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

All times shown according to UTC.

Time Nick Message
00:04 barrucadu I'm trying to relate set cardinality to the BNF notion of cardinality, but I'm not really sure how to go about it
00:04 barrucadu Specifically, I want to show ∀ x y. (card x ≤ card y ⟶ ordLeq3 (card_of x) (card_of y))
00:31 wagle joined #isabelle
00:32 wagle joined #isabelle
01:04 wagle joined #isabelle
01:35 wagle joined #isabelle
02:48 barrucadu Never mind, I rephrased the problem and got it working
02:48 barrucadu "finite x ⟹ finite y ⟹ card x ≤ card y ⟹ ordLeq3 (card_of x) (card_of y)" by (meson card_le_inj card_of_ordLeq)
03:33 barrucadu I'm now stuck trying to prove "⋀ m. finite (Map.dom m) ⟹ card {(a, b). m a = Some b} = card (Map.dom m)", any help would be appreciated
06:18 barrucadu Again, I got it after reformulating it a little: https://gist.github.com/barrucadu/64c4c9f0ddbb9475252c
10:02 ThreeOfEight barrucadu: http://downthetypehole.de/paste/gm2hl6Ml
10:03 ThreeOfEight You don't even need finiteness
10:06 barrucadu Wow, that's much smaller
10:06 barrucadu What is … there?
10:12 ThreeOfEight that refers to the right-hand side of the last equation
10:12 barrucadu Ahh, that's convenient
10:12 ThreeOfEight (actually, it matches the last proposition against "?P ?x ?y" and returns ?y)
10:12 barrucadu Thanks
10:13 ThreeOfEight (so if it's something like "x = y" or "x <= y", you will get the y)
10:13 ThreeOfEight ... also works
23:13 wagle joined #isabelle
23:43 wagle joined #isabelle

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