The tree configuration is not always taken into account

francoisthire commented 10 months ago

Here is a not minimal snippet and we can see the that the configuration is not taken the same way in the different rules:

#figure(caption:"LF Type system")[
  #set text(size: 15pt)
  #let config = prooftrees.tree_config(premises_spacing: 10pt, vertical_spacing:5pt)

#rect(stroke:blue, inset:10pt, radius:8pt)[
#prooftrees.tree(tree_config:config,
  prooftrees.axi[],
  prooftrees.uni[$emptyset tack "Type" : "Kind"$]
)

#prooftrees.tree(tree_confing:config,
  prooftrees.axi[$Gamma tack t : A$],
  prooftrees.axi[$Gamma tack B : "Type"$],
  prooftrees.bin[$Gamma, x : B tack t : A$]
)

#prooftrees.tree(tree_confing:config,
  prooftrees.axi[$Gamma tack A : "Type"$],
  prooftrees.axi[$Gamma tack B : "Type"$],
  prooftrees.bin[$Gamma tack Pi (x : A) arrow B : "Type" $]
)

#prooftrees.tree(tree_config:config,
  prooftrees.axi[$Gamma tack A : "Type"$],
  prooftrees.axi[$Gamma tack B : "Kind"$],
  prooftrees.bin[$Gamma tack Pi (x : A) arrow B : "Kind" $]
)

#prooftrees.tree(tree_config:config,
  prooftrees.axi[$Gamma, x : A tack t : B$],
  prooftrees.axi[$Gamma tack Pi (x : A) arrow B : s$],
  prooftrees.bin[$Gamma tack lambda (x : A), t : Pi (x : A) arrow B$]
)

#prooftrees.tree(tree_config:config,
  prooftrees.axi[$Gamma tack f : Pi (x : A) arrow B$],
  prooftrees.axi[$Gamma tack a : A$],
  prooftrees.bin[$Gamma tack f a : B{x arrow.l a}$]
)

#prooftrees.tree(tree_confing:config,
  prooftrees.axi[$Gamma tack t : A$],
  prooftrees.axi[$Gamma tack B : s$],
  prooftrees.axi[$Gamma tack A attach(=, br:beta) B $],
  prooftrees.tri[$Gamma tack Pi (x : A) arrow B : "Kind" $]
)
]
]

francoisthire commented 10 months ago

I was not able to see the typos :face_exhaling: :facepalm:

david-davies commented 10 months ago

I'm re-opening this cause I think there still are cases it's ignored

david-davies / typst-prooftree

The tree configuration is not always taken into account #2