Inference rules | Typst | Page 1

Hi! Im trying to display inference rules using typst. First image is an example of what i'm trying to do, and second image is what i managed to do using tables (and the tablex package).
Im not entirely satisfied with the lines being longer than necessary. Did anyone already manage to do something similar by any chance?

Here is the code if you want to try it :


#import "tablex.typ": *

#let rule(name: [], ccl, ..prem) = {
  let prem = prem.pos()
  let n = prem.len()
  if n == 0 { n = 1 }
  stack(dir: ltr,
  gridx(
    inset: 0pt,
    columns: n,
    align: bottom+center,
    column-gutter: 1cm,
    ..prem,
    colspanx(n, " "), 
    hlinex(stroke: 0.5pt, start: 0, end: 3),
    colspanx(n, " "), 
    colspanx(n, ccl)
  ), if name != none {align(bottom, box(inset: (left: 2pt, bottom: 1em), name))} else [])
}


#align(center,
rule(name: $->_i$,
  $tack (p -> q) -> not (p and not q)$,
  rule(name: $not_i$,
    $p -> q tack   not (p and not q)$,
    rule(name: $not_e$,
      $p -> q, p and not q tack bot$,
      rule(name: $->_e$,
        $Gamma tack q$,
        rule(name: "ax",
          $Gamma tack p -> q$
        ),
        rule(name: $and_e^g$,
          $Gamma tack p$,
          rule(name: "ax",
            $Gamma tack p and not q$
          )
        )
      ),
      rule(name: $and_e^d$,
        $Gamma tack not q$,
        rule(name: "ax", 
          $Gamma tack p and not q$
        )
      )
    )
  )
)
)

#Inference rules