Missing line above `axi`

[MDLC01]

The problem

When laying out a proof tree, no line is displayed above axioms. However, I often want a line above those. Typically, I want one above axioms, but none above the prerequisites of a rule, when defining a rule. So there is need for both cases.

The solution

axi / nary.with(0) should show a line by default, and there should be another function (or maybe simply a parameter for axi) for when you don't want the line above. This would also let the user add labels to axioms, which is currently impossible.

An alternative solution to adding a new function is to accept arguments that are not wrapped inside a nary (or similar) function, and tread them as axi currently are, and make axi display a line above. For example:

// This would display a line above.
#tree(
  axi[...],
)

// This would not.
#tree(
  [...],
)

// Then, you can define a new rule like that (no line above the prerequisites):
#tree(
    [$Gamma tack A$],
    [$Gamma tack B$],
  bin[$Gamma tack A and B$],
)

// If you want a line above the prerequisites:
#tree(
    axi[$Gamma tack A$],
    axi[$Gamma tack B$],
  bin[$Gamma tack A and B$],
)

Temporary solution

A temporary solution is to replace the axi with an empty axi, followed by a uni:

#tree(
    axi[],
  uni(right_label: [(ax)])[$A tack A$],
)

[david-davies]

This looks a good idea, although it breaks from bussproofs's api. I like the first solution, essentially extending any nary function with a flag to turn off the line. The second solution could be a syntactic sugar into the first e.g. axi.with(no_line: true): I don't think it works as a general solution because, as you mentioned, it prevents the user from adding labels.

fwiw your temporary solution is one-to-one with a latex macro I have :)