Andrej Bauer

Can you give an example which shows what's incorrect about thunk and force? Note that we have both `let` and `do`. Your description of `let` sounds like what `do` is...

Ugh, this repository is severely outdated. I should get rid of it, actually.

A separate branch, one per language.

It would be better to have one issue per language, so you we can close them, and perhaps organize them into a milestone.

What's the point of a separate repository? It'll just become obsolete. I still think the best way is to just fork this repository, add a language (half baked or not),...

Thanks. 1. There are some stylistic changes that should be made before we can pull this (such as not opening the `Syntax` module everywhere). 2. There are too few comments...

I think I know how to do this. I'd like to keep the languages nice and clean, but at the same time I don't want to reject other people's contributions...

The [guidelines are here](http://plzoo.andrej.com/contributions.html). You are using `open Syntax` all over the place (point 9). You do not have interface files (point 7). The non-stylistc comment is that I would...

Many thanks. I think there's some value in having, e.g., both a non-commutative and a commutative field, for comparison. But I like the idea that the non-efficient theories should be...

This bug bugs me too. It's created by the use of the [markdown-table](https://github.com/wooorm/markdown-table) package, which is maintained by @wooorm. Maybe we should ask the maintainer what a possible solution might...