(*** Exercice 1 ***) (*** Exercice 2 ***) let leftlabel s = "\\LeftLabel{\\footnotesize[\\textcolor{green!70!black}{\\textsc{"^s^"}}]}\n" let derivation_tree t = let rec derivation_tree_int t = match t with | TmZero | TmTrue | TmFalse -> "\\AxiomC{}\n" ^(leftlabel "Ax") ^"\\UnaryInfC{" ^(term_to_string t)^"}\n" | TmSucc u -> (derivation_tree_int u) ^(leftlabel "Succ") ^"\\UnaryInfC{"^(term_to_string t)^"}\n" | TmIsZ u -> (derivation_tree_int u) ^(leftlabel "IsZero") ^"\\UnaryInfC{"^(term_to_string t)^"}\n" | TmIf(i,u,e) -> (derivation_tree_int i) ^(derivation_tree_int u) ^(derivation_tree_int e) ^(leftlabel "If") ^"\\TrinaryInfC{"^(term_to_string t)^"}\n" in "\\begin{prooftree}\n\sffamily\n" ^(derivation_tree_int t) ^"\\end{prooftree}\n";; (*** Exercice 3 ***)