User talk:DanielKLee

From The Twelf Project
Jump to: navigation, search

My To-Do/Wish List

  • Fill in the %trustme example for the %trustme article
  • Tutorial: Introductory series. Tutorials for people who start knowing nothing about Twelf
  • Tutorial: Manually proving substitution lemmas [for dependently typed languages], i.e. the slide

You should add that stuff to the page I made at Project:To do - I've already listed your adoption of the %trustme article — Rob (and his talk) 07:43, 22 September 2006 (MST)


I deleted the fictonal blog entries - until we know what we're doing, when we're doing it, and where things are permanently hosted, I don't think we should spend time on the blog - it's just something I wanted to make sure was there as part of the equation. In any case, my thought is that blog updates will be something along the lines of "we've now added a tutorial describing closure conversion," a paragraph about why that's important/hard/easy, and a link to a page on the wiki, where we have pretty things like syntax highlighting.

You can find links that let you edit individual sections of the front page at Talk:Main Page, a fact which I have added to Project:Contributing.

Also, was something like Project:Style guide what you were thinking about? We also should think about a Twelf style guide, which also might have been what you were thinking about. - Rsimmons 09:05, 6 September 2006 (MST)


You were going to add information on anon CVS download when you got a chance, just a reminder :). — Rob (and his talk) 19:49, 7 September 2006 (MST)

Simpler version of "slide"

Would a simpler version of your "slide" example be the storetype weakining issue I described at ? One of my to-dos is to transwiki things from the old wiki; I can expand that example if it would be useful as a simple case of what you're describing. Alternatively, if what you're describing does what I did better, I could hold off on the transwiki. — Rob (and his talk) 10:32, 22 September 2006 (MST)

That is the non-dependent types version of the technique. I was planning on doing a more generalized explanation of this (the current write-up is very Rob's thesis specific and fails to call the "extra induction" a substitution lemma), which would lead into the version for dependent types. The "slide" substitution for dependent types isn't as generally useful as explicit contexts, but it's among the most badass Twelf hacks I know. If you don't mind, I'd like to take this one over, but definitely do transwiki the other answers from the old Q&A.
'swhy I asked. Go for it, and horray for general solutions! 11:57, 22 September 2006 (MST)

can vs. expressiveness

Do you still call the can- lemmas expressiveness lemmas? That section should include a link to a page about expressiveness lemmas, or whatever we call them, even if it's a redlink for now. — Rob (and his talk) 14:42, 23 September 2006 (MST)

I'm unaware of any category of lemmas called expressiveness lemmas. Is this something from the old wiki? I can't seem to find a reference to them. --DanielKLee 14:51, 23 September 2006 (MST)
Eek - susmit actually called them "Effectiveness lemmas" - whatever it is you call the can- lemmas, I feel like they have, or should have, some name. — Rob (and his talk) 15:02, 23 September 2006 (MST)

Twelf coffee

I'm at home today, so no coffee for me. Doesn't seem like anybody did anything since last week anyway. ;)  — Tom 7 16:41, 4 October 2006 (EDT)

"Group" doesn't work anymore

Using include="..." works similarly - I had to change it to handle multiple inheritance. See the TwelfTag page for an explanation of the modified feature, I'm sorry about that. — Rob (and his talk) 17:22, 11 October 2006 (EDT)

Oh I see... *cry* --DanielKLee 17:34, 11 October 2006 (EDT)
Hang on - I'm going to make "group" a silent alias for "include". Just don't use it anymore! — Rob (and his talk) 17:38, 11 October 2006 (EDT)
Done. Don't say I never did anything for you :). — Rob (and his talk) 17:44, 11 October 2006 (EDT)
Thanks!! --DanielKLee 17:45, 11 October 2006 (EDT)