sail-to-lean: annotate data type annotations (including quantifiers)

[tobiasgrosser]

Look over all files in https://github.com/rems-project/sail/tree/sail2/lib, e.g., https://github.com/rems-project/sail/blob/sail2/lib/flow.sail.

Here an example PR: https://github.com/rems-project/sail/pull/754/files

We may want to use HAdd.add instead of Int.add

[jprider63]

@benjaminselfridge is actually working on this, but I don't seem to be able to assign it to him. @Alasdair would you please add him to the repository?

[jprider63]

From @javra:

New Lean defs go here: src/sail_lean_backend/Sail/Sail.lean

[benjaminselfridge]

We're starting a branch here: https://github.com/GaloisInc/sail/blob/feature/lean_external_arith/lib/arith.sail

Does the initial commit I made look sane to you?

[javra]

Looks good! There's a better abs in Mathlib, but since we don't want to depend on it, that's not an option.

You could also, in Sail.lean, add intAbs, define it as the composition you used, and thant refer to that in the annotation.