- | nd_id0 => indent +++ "% nd_id0 " +++ eol
- | nd_id1 h' => indent +++ "% nd_id1 "+++ judgments2latex h +++ eol
- | nd_weak h' => indent +++ "\inferrule*[Left=ndWeak]{" +++ judgment2latex h' +++ "}{ }" +++ eol
- | nd_copy h' => indent +++ "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++
- "}{"+++judgments2latex c+++"}" +++ eol
- | nd_prod h1 h2 c1 c2 pf1 pf2 => indent +++ "% prod " +++ eol +++
- indent +++ "\begin{array}{c c}" +++ eol +++
- (nd_toLatex pf1 (" "+++indent)) +++
- indent +++ " & " +++ eol +++
- (nd_toLatex pf2 (" "+++indent)) +++
- indent +++ "\end{array}"
- | nd_comp h m c pf1 pf2 => indent +++ "% comp " +++ eol +++
- indent +++ "\begin{array}{c}" +++ eol +++
- (nd_toLatex pf1 (" "+++indent)) +++
- indent +++ " \\ " +++ eol +++
- (nd_toLatex pf2 (" "+++indent)) +++
- indent +++ "\end{array}"
- | nd_cancell a => indent +++ "% nd-cancell " +++ (judgments2latex a) +++ eol
- | nd_cancelr a => indent +++ "% nd-cancelr " +++ (judgments2latex a) +++ eol
- | nd_llecnac a => indent +++ "% nd-llecnac " +++ (judgments2latex a) +++ eol
- | nd_rlecnac a => indent +++ "% nd-rlecnac " +++ (judgments2latex a) +++ eol
- | nd_assoc a b c => ""
- | nd_cossa a b c => ""
- | nd_rule h c r => rule2latex h c r
+ | nd_id0 => rawLatexMath indent +++
+ rawLatexMath "% nd_id0 " +++ eolL
+ | nd_id1 h' => rawLatexMath indent +++
+ rawLatexMath "% nd_id1 "+++ judgments2latex h +++ eolL
+ | nd_weak h' => rawLatexMath indent +++
+ rawLatexMath "\inferrule*[Left=ndWeak]{" +++ toLatexMath h' +++ rawLatexMath "}{ }" +++ eolL
+ | nd_copy h' => rawLatexMath indent +++
+ rawLatexMath "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++
+ rawLatexMath "}{"+++judgments2latex c+++rawLatexMath "}" +++ eolL
+ | nd_prod h1 h2 c1 c2 pf1 pf2 => rawLatexMath indent +++
+ rawLatexMath "% prod " +++ eolL +++
+ rawLatexMath indent +++
+ rawLatexMath "\begin{array}{c c}" +++ eolL +++
+ (nd_toLatexMath pf1 (" "+++indent)) +++
+ rawLatexMath indent +++
+ rawLatexMath " & " +++ eolL +++
+ (nd_toLatexMath pf2 (" "+++indent)) +++
+ rawLatexMath indent +++
+ rawLatexMath "\end{array}"
+ | nd_comp h m c pf1 pf2 => rawLatexMath indent +++
+ rawLatexMath "% comp " +++ eolL +++
+ rawLatexMath indent +++
+ rawLatexMath "\begin{array}{c}" +++ eolL +++
+ (nd_toLatexMath pf1 (" "+++indent)) +++
+ rawLatexMath indent +++
+ rawLatexMath " \\ " +++ eolL +++
+ (nd_toLatexMath pf2 (" "+++indent)) +++
+ rawLatexMath indent +++
+ rawLatexMath "\end{array}"
+ | nd_cancell a => rawLatexMath indent +++
+ rawLatexMath "% nd-cancell " +++ (judgments2latex a) +++ eolL
+ | nd_cancelr a => rawLatexMath indent +++
+ rawLatexMath "% nd-cancelr " +++ (judgments2latex a) +++ eolL
+ | nd_llecnac a => rawLatexMath indent +++
+ rawLatexMath "% nd-llecnac " +++ (judgments2latex a) +++ eolL
+ | nd_rlecnac a => rawLatexMath indent +++
+ rawLatexMath "% nd-rlecnac " +++ (judgments2latex a) +++ eolL
+ | nd_assoc a b c => rawLatexMath ""
+ | nd_cossa a b c => rawLatexMath ""
+ | nd_rule h c r => toLatexMath r