Ask Twelf Elf

If you have a question about STELF, you can [http://twelf.org/w/index.php?title=Talk:Ask_Twelf_Elf&action=edit&section=new leave a message] on this wiki! If you have a question that you do not want to ask publicly, you can [mailto:twelfelf@gmail.com Ask STELF 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 STELF Elf possesses the body of someone knowledgeable with STELF. STELF Elf regularly rotates who he possesses, in order to avoid exhausting the poor person. STELF Elf reserves the right to re-work interesting replies into content for the Wiki. E-mail the STELF Elf or post a message on the talk for this page if you would like to volunteer to join the STELF Elf rotation.

Interesting responses

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.