agda2vec introduces extra empty lines

[williamdemeo]

Description

This closes issue #653.

(It may be as simple as removing the extra new line character + \n from the file.write line in the write_file function.)

Checklist

• Commit sequence broadly makes sense and commits have useful messages
• Any semantic changes to the specifications are documented in CHANGELOG.md
• Code is formatted according to CONTRIBUTING.md
• Self-reviewed the diff

[williamdemeo]

So we can use the List type annotation and type aliases in agda2vec.py:

from typing import List, TypeAlias
StrVec: TypeAlias = List[str]

[williamdemeo]

This makes the code more transparent and much easier to understand, imo.

[carlostome]

I agree that making the bindings' type explicit makes it easier to understand the rule.

[carlostome]

LGTM

[williamdemeo]

No need for the extra indentation/whitespace since we're not relying on agda to handle alignment here.

[carlostome]

LGTM.

There seems to be a small aligning glitch, which was already present before, in that sometimes lines containing vertical vectors aren't aligned with their surroundings. For example, see Ratify-Continue and Ratify-Reject in Figure 44.

[carlostome]

I agree that making the bindings' type explicit makes it easier to understand the rule.

[carlostome]

LGTM

[williamdemeo]

LGTM.

There seems to be a small aligning glitch, which was already present before, in that sometimes lines containing vertical vectors aren't aligned with their surroundings. For example, see Ratify-Continue and Ratify-Reject in Figure 44.

You're absolutely right. I'm not sure how hard this would be to fix, but it would surely involve making the script more sophisticated (or, rather, less dumb). Right now agda2vec throws away some alignment information (in the form of the Agda generated escape sequences, like \>[981I][@{}l@{\AgdaIndent{0}}]). Perhaps the next improvement to the script should be to actually try to make use of these alignment macros.