Slight confusions in documentation

[mikeshulman]

I know it's hard to keep documentation up to date with a changing system, but I just thought I would help by pointing out a few issues with http://www.andromeda-prover.org/meta-language.html:

1. The section on dynamic variables says "The current value is accessed with simply x" but in fact it seems that you have to write current x.
2. The section on operations correctly says that an operation is declared with its input and output types, but the example of the Hole operation instead declares it by giving a single number (its input arity?).
3. In the description of the rule beta_step, the order of arguments in the displayed syntax differs from the order of the bullet points below it.
4. The sections on matching under binders, mutable references, and declarations look as though they are supposed to contain bullet lists, but maybe some markdown syntax didn't get correctly parsed into html.
5. The section on lists says "lists are heterogeneous in the sense that they may contain values of different shapes" but that does not seem to be true any more.

[mikeshulman]

Two more:

6. It appears that hypotheses is treated like a dynamic variable, so that you have to write current hypotheses to get the actual list of hypotheses.
7. Even once the example Hole operation is fixed by declaring it as Hole : judgment and having hole_filler call current hypotheses rather than hypotheses, it needs a further fix because, as stated in the section on operation cases, the form | op p₁ ... pᵢ : p => c matches p against Some t when invoked in checking mode at type t, not t itself. I think the simplest thing to do is just declare it to handle Hole : Some ?t instead of Hole : ?t.

[mikeshulman]

8. I cannot figure out how to access the "external" functions. The syntax described in the documentation certainly doesn't work (except for the special case print X).