proof_trees.typ

#let proof(
  name: none,
  line: line(length: 100%),
  above,
  below,
  elem_padding: 1.5em,
  line_padding: .3em,
  name_padding: .4em,
) = style(styles => {
  // Make reassignable
  let name = name;
  let above = above;
  let below = below;

  // Normalize arguments
  if type(above) != "array" {
    above = (above,)
  }
  if type(below) == "array" {
    assert(
      below.len() == 1,
      message: "there must be exactly one element below the inference line"
    )
    below = below.at(0)
  }

  // Wrap arguments in equations
  if name != none {
    name = $ name $
  }
  above = above.map(it => $ it $)
  below = $ below $

  // Aaand... render

  let above = stack(
    dir: ltr,
    spacing: elem_padding,
    ..above,
  )

  let above_w = measure(above, styles).width
  let below_w = measure(below, styles).width
  let line = box(width: calc.max(above_w, below_w), line)

  let main = stack(
    dir: ttb,
    spacing: line_padding,
    above,
    line,
    below,
  )

  let result = if name == none {
    main
  } else {
    let line_h = measure(line, styles).height;
    let below_h = measure(below, styles).height
    let name_h = measure(name, styles).height
    let dy = below_h + line_padding + line_h / 2 - name_h / 2;
    stack(
      dir: ltr,
      spacing: name_padding,
      main,
      move(dy: -dy, name)
    )
  }

  align(center + bottom, result)
})

#let intro(what) = what + "I"
#let elim(what) = what + "E"

#let zigzag(
  width: 100%,
  height: 0.3em,
  segments: 100,
  segment_width: 0.2em,
) = {
  let points = ()
  for n in range(0, segments + 1) {
    let x = n * segment_width
    let y = if calc.even(n) { 0% } else { 100% }
    points.push((x, y))
  }
  box(
    width: 100%,
    height: height,
    clip: true,
    inset: (y: 0.05em),
    outset: 0em,
    path(..points),
  )
}