Skip to content

Commit 7103ef2

Browse files
committed
update: partly handle hypotheses
1 parent fa90e13 commit 7103ef2

2 files changed

Lines changed: 9 additions & 5 deletions

File tree

‎docs/usage/natural-deduction.md‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -88,17 +88,17 @@ print(deriv.latex())
8888

8989
$$
9090
\begin{prooftree}
91-
\AxiomC{$A$}
91+
\AxiomC{$[A]$}
9292
\RightLabel{$\lor$I}
9393
\UnaryInfC{$A \lor C$}
94-
\AxiomC{$B$}
95-
\RightLabel{$\to$E}
9694
\AxiomC{$B \to C$}
95+
\AxiomC{$[B]$}
96+
\RightLabel{$\to$E}
9797
\BinaryInfC{$C$}
9898
\RightLabel{$\lor$I}
9999
\UnaryInfC{$A \lor C$}
100-
\RightLabel{$\lor$E}
101100
\AxiomC{$A \lor B$}
101+
\RightLabel{$\lor$E}
102102
\TrinaryInfC{$A \lor C$}
103103
\end{prooftree}
104104
$$

‎mathesis/deduction/natural_deduction/natural_deduction.py‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -114,7 +114,11 @@ def latex(self, number=False, arrow=r"\Rightarrow"):
114114
tmpl = r"\BinaryInfC{{${}$}}"
115115
elif len(node.children) == 3:
116116
tmpl = r"\TrinaryInfC{{${}$}}"
117-
output += label_part + tmpl.format(node.name.fml.latex()) + "\n"
117+
118+
fml = str(node.name.fml.latex())
119+
if hasattr(node, "hyp") and node.hyp:
120+
fml = f"[{fml}]"
121+
output += label_part + tmpl.format(fml) + "\n"
118122

119123
return """\\begin{{prooftree}}\n{}\\end{{prooftree}}""".format(output)
120124

0 commit comments

Comments
 (0)