Ask Twelf Elf
If you have a question about Twelf, you can leave a message on this wiki! If you have a question that you do not want to ask publicly, you can Ask Twelf Elf by email. You should get a reply within 48 hours. Probably sooner. If your question involves diagnosing a particular piece of code, it is very helpful if you can send in enough code that we can re-produce the issue on our own machines.
At any given time, the spirit of Twelf Elf possesses the body of someone knowledgeable with Twelf. Twelf Elf regularly rotates who he possesses, in order to avoid exhausting the poor person. Twelf Elf reserves the right to re-work interesting replies into content for the Wiki. E-mail the Twelf Elf or post a message on the talk for this page if you would like to volunteer to join the Twelf Elf rotation.
Some responses to questions turn into other forms of documentation; the rest are collected here.
- Short Answers - collected answers that have not (yet) been turned into their own pages.
- Manipulating proof witnesses - running a %solve creates a proof object if it is successful. But what if you want to manipulate such proof objects within the context of a single %solve? The cost of the ability to do this is writing a bunch of effectiveness lemmas - in this case, if you were working with relations which were not total functions, they could be called effectiveness relations.
- Concrete representations - higher-order abstract syntax is a convenient way to approach languages with binding, but it is possible to imagine a problem where manipulating a fully concrete object without binding is simpler. In these cases, it is possible to establish a bijection between your HOAS terms and de Bruijn versions of the same terms.