Variables and sections (Coq-style)

[fizruk]

This introduces Coq-style variables and sections.
See #37 for some comparison and discussion around variables in Lean vs Coq vs Rzk.

• Named sections (#section <name>, ended with #end <name>)
  • Check that names match
• Unnamed sections (#section, ended with #end)
• Single-variable command (#variable x : T)
• Multi-variable command (#variables x y z : T)
• Issue an error if a variable is used implicitly (not mentioned in its type or body)
  • Support explicit declaration of (implicitly) used variables to suppress the error
• Issue an error if a variable is never used
• Documentation
• Fix free vars extraction for typed terms (have to get free vars from types recursively, possibly should be cached in TypeInfo)
• Tests (would be nice to have some)

Note that point variables with tope restrictions and patterns are not supported.
That is you cannot define the following:

#variable {t : I | psi t}   -- ERROR: tope restrictions are not supported!
#variable s : Δ²            -- ERROR: tope restrictions are not supported!
#variable (t, s) : 2 * 2    -- ERROR: patterns are not supported!

[fizruk]

Example of a warning for an implicit assumption in the following definition:

https://github.com/fizruk/rzk/blob/018e70deb20e1a6bbd35fbe373d20634ba2d362c/docs/docs/rzk-1/recId.md?plain=1#L144-L162

[ 19 out of 20 ] Checking #define recId
Warning: implicit assumption
  r : relfunext2
used in definition of
  recId

EDIT: this is now an error rather than a warning.

[fizruk]

The warning can now be suppressed by explicitly mentioning used variables (it is sufficient to only mention variables that are used implicitly):

#def recId uses (r) -- we declare that recId is using r on purpose
    (a_psi : (t : psi) -> A t)
    (a_phi : (t : phi) -> A t)
    (e : {t : I | psi t /\ phi t} -> a_psi t = a_phi t)
  : {t : I | psi t \/ phi t} -> A t
  := ...