Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2014-09-10

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

All times shown according to UTC.

Time Nick Message
02:05 gattschardo joined #isabelle
09:49 redlizard joined #isabelle
09:52 redlizard When importing a locale as a basis of a new locale, isabelle helpfully renames all type variables occurring in the base locale to 'a 'b 'c and such. How can I tell it to stop doing that and use my descriptive names instead?
09:57 gattschardo i have not worked with locales yet unfortunately
09:58 gattschardo can you maybe just give names for the type variables when you import the locale
09:58 gattschardo like for example when you have a "cases" proof in isar as "case (Casename Var1 Var2)"
09:59 redlizard According to the ISAR reference there is *some* facility for this, but I have a hard time making sense of it.
09:59 gattschardo i see
10:00 gattschardo unfortunately this channel is mostly idle, but you might have some luck on stackoverflow.com
10:00 redlizard There is import with for..end, but I don't really know what that means.
10:00 redlizard Yeah, I noticed.
10:01 gattschardo me neither, i'm very much a beginner in isabelle myself
10:01 redlizard Looks like this is the first actual interaction between two people in this channel since April.
10:01 gattschardo i was hoping to pick up some hints in this channel, but yeah
10:01 gattschardo its somewhat unlikely
10:02 gattschardo yup, going through the logs i was just seeing the join - question - no answer - leave pattern
10:14 redlizard Oh, apparently a "constrains" clause can do it.
10:14 redlizard Which is deprecated in favour of a "for" clause, but that one doesn't appear to do what I want it to do.
10:15 redlizard Oh well.
11:15 dmiles_afk joined #isabelle
22:26 dnm joined #isabelle
23:15 dmiles_afk joined #isabelle

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