Camelia, the Perl 6 bug

IRC log for #isabelle, 2011-12-21

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

All times shown according to UTC.

Time Nick Message
01:24 wagle joined #isabelle
05:59 eyebloom joined #isabelle
05:59 monochrom except I don't know who is actually around to answer questions. I can't answer questions.
05:59 eyebloom Gotcha
06:01 eyebloom I'm working my way through the tutorial and using Emacs/Proof-General/Isabelle and finding that it never wants to parse special characters.
06:02 eyebloom In most cases, such as boolean operators, I've found that there are alternatives that work fine
06:02 eyebloom But characters like "forall" ∀ are causing lots of problems.
06:02 ski joined #isabelle
06:03 eyebloom So just curious if anyone has experience with this. Or knows of alternatives to the ∀ character for example.
06:17 monochrom joined #isabelle
06:50 eyebloom joined #isabelle
07:25 eyebloom Got it, one just needs to type the latex/ascii name into emacs
07:30 larsrh you can also try the jEdit interface if you wish
07:30 larsrh it offers code completion for that
16:21 eyebloom joined #isabelle
17:41 eyebloom joined #isabelle
18:28 eyebloom Thanks, Emacs seems to be working the best
18:28 eyebloom So far
18:54 eyebloom One other question: Can one define a datatype as a list of another type:
18:55 eyebloom As in: type_synonym vertex = nat
18:55 eyebloom datatype adj = [vertex]
18:55 eyebloom I get an outer syntax error when I try to do this.
19:23 eyebloom joined #isabelle
21:34 eyebloom joined #isabelle
22:27 eyebloom Can tuples be used for pattern matching in a function definition in Isabelle?
23:33 larsrh eyebloom: for your datatype problem, try `vertex list`
23:33 larsrh eyebloom: also, you can write `foo (a, b) = ...` if `foo` takes a tuple
23:33 larsrh although "thou shalt curry your functions" :)
23:33 eyebloom What do you mean by vertex list?
23:34 larsrh `vertex list` is the type of a list containing elements of type `vertex`
23:34 eyebloom I see.
23:34 larsrh the question is whether you want a synonym or a wrapper for that
23:34 eyebloom I'm trying to verify operations on inductive graphs.
23:35 eyebloom The underlying tuple is a called a context
23:35 larsrh maybe `datatype adj = Adj "vertex list"`
23:35 eyebloom In haskell its ([vertex], vertex, a, [vertex])
23:36 eyebloom So I'd like to be able to deconstruct a context when I pass it to a function
23:36 larsrh datatype 'a context = Context "vertex list" vertex "'a" "vertex list" should do it
23:36 larsrh that would be roughly equivalent to a newtype in haskell
23:37 eyebloom I see, just avoid tuples altogether basically
23:37 larsrh no, not really
23:37 larsrh but if you have a 4-tuple it might be a good idea to introduce a separate datatype
23:38 larsrh to communicate to the reader what you mean
23:39 eyebloom Why do you leave vertex out of quotes there/
23:39 eyebloom ?
23:39 larsrh sometimes I'
23:40 larsrh m not sure when to drop quotes :)
23:40 larsrh I'm just an advanced beginner :)
23:40 eyebloom Me too
23:41 eyebloom Beggining begginer
23:41 eyebloom And unable to spell

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