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
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.
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)
Simpler version of "slide"
Would a simpler version of your "slide" example be the storetype weakining issue I described at http://fp.logosphere.cs.cmu.edu/twelf/?n=Answers.WorldsAndWeakening ? 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! 126.96.36.199 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)
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)
- Thanks!! --DanielKLee 17:45, 11 October 2006 (EDT)