Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-08-15

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

All times shown according to UTC.

Time Nick Message
01:47 ilbot3 joined #isabelle
01:47 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
01:52 Damaki joined #isabelle
11:14 silver joined #isabelle
11:46 Damaki joined #isabelle
13:30 Damaki joined #isabelle
16:24 Damaki joined #isabelle
19:59 Damaki joined #isabelle
21:59 int-e Is there a good way of bringing the constructors of Enum.finite_3 (for example) into scope inside a proof? I have used  let ?a1 = Enum.finite_3.a\<^sub>1 and ?a2 = Enum.finite_3.a\<^sub>2 and ?a3 = Enum.finite_3.a\<^sub>3  which makes them easy to type but I would like to actually bring the a\<^sub>1 into scope, if possible...

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