Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-03-16

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

All times shown according to UTC.

Time Nick Message
02:46 fracting1 joined #isabelle
07:06 fracting joined #isabelle
08:11 fracting joined #isabelle
09:44 fracting joined #isabelle
12:05 fracting joined #isabelle
12:41 chuchucorny how can I `cast' a 16 word to a 128 word?
12:46 chuchucorny oh, just found ucast. thx
12:51 larsrh ThreeOfEight: you can use Proof.refine to apply a method to a state
12:52 larsrh e.g. Proof.theorem ... |> Proof.refine your_method_here |> Seq.hd
12:54 larsrh you can turn a tactic into a method with METHOD
12:54 larsrh (or SIMPLE_METHOD, or SIMPLE_METHOD')
12:56 ThreeOfEight kthx
12:56 ThreeOfEight I somehow didn't find that in the implementation manual
12:57 ThreeOfEight I'm starting to think this command that I'm implementing might be overkill
12:57 ThreeOfEight …just a little bit
12:57 larsrh Are you implying that there are gaps in the implementation manual?
12:58 larsrh snark aside, it's in isar-ref, §6.4.4
12:59 ThreeOfEight …what
12:59 ThreeOfEight oh wait
13:00 ThreeOfEight isar-ref?
13:00 ThreeOfEight not the implementation manual?
13:00 ThreeOfEight …łhy
13:00 ThreeOfEight *why
13:03 fracting1 joined #isabelle
13:46 fracting joined #isabelle
13:49 fracting joined #isabelle
13:54 ThreeOfEight larsrh: what version of isar-ref are you referring to?
13:54 ThreeOfEight I can't find any mention of Proof.refine in isar-ref or implementation
13:54 ThreeOfEight it expects a "method.text" and I have no idea what that is
14:00 ThreeOfEight okay, I can use Method.Basic and Seq.the_result, but damn, that is ugly
14:10 dmiles joined #isabelle
14:20 fracting joined #isabelle
14:34 larsrh ThreeOfEight: method.text?!
14:35 larsrh Oh wait
14:35 larsrh grep the BNF sources for refine
14:35 larsrh they use it in some places
17:03 fracting joined #isabelle
17:10 chuchucorny how can I view the type of functions in the proof state?
17:10 chuchucorny I have something like "of_bl (to_bl (of_bl (to_bl (of_bl ..."
17:11 chuchucorny I'm interested in the word length which of_bl returns
17:12 larsrh Ctrl-Hover doesn't show the type?
17:15 chuchucorny nope, unfortunately not
17:15 chuchucorny of_bl :: "bool list ⇒ 'a::len0 word"  so I'm interested in the concrete number for 'a::len0
17:18 larsrh yeah, understood
17:18 larsrh The question I'm asking myself is: why isn't this in the markup
17:20 chuchucorny probably there aren't many users who work with the word type
17:21 larsrh The answer is likely to be in syntax_phases.ML
17:21 chuchucorny sledgehammer is also quite unusable for anything with words
17:21 larsrh But my Pure-fu is too weak to understand inner syntax
17:22 larsrh AFAICT there's no standard way to get the information you want
17:23 larsrh If you're feeling adventurous, try ML_val ‹@{Isar.goal} |> #goal |> Thm.prop_of›
17:23 larsrh This will print the goal state as a raw term
17:23 larsrh optionally preceded by using [[ML_print_depth=100]]
17:25 chuchucorny then I will probably continue to use my side channels
17:27 larsrh Your side channels?
17:28 chuchucorny writing type annotations everywhere, not using generic rules
17:35 ThreeOfEight larsrh: I'm getting the impression that it's impossible to use curly braces in outer syntax
17:35 ThreeOfEight because { is a command
17:35 ThreeOfEight any thoughts on that?
17:40 larsrh ThreeOfEight: you can't
18:54 ThreeOfEight meh.
22:17 ilbot3 joined #isabelle
22:17 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/
23:30 Damaki joined #isabelle

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