+
+(* escapifies any characters which might cause trouble for LaTeX *)
+Variable sanitizeForLatex : string -> string.
+ Extract Inlined Constant sanitizeForLatex => "sanitizeForLatex".
+Inductive Latex : Type := latex : string -> Latex.
+Instance LatexToString : ToString Latex := { toString := fun x => match x with latex s => s end }.
+Class ToLatex (T:Type) := { toLatex : T -> Latex }.
+Instance StringToLatex : ToLatex string := { toLatex := fun x => latex (sanitizeForLatex x) }.
+Instance LatexToLatex : ToLatex Latex := { toLatex := fun x => x }.
+Definition concatLatex {T1}{T2}(l1:T1)(l2:T2){L1:ToLatex T1}{L2:ToLatex T2} : Latex :=
+ match toLatex l1 with
+ latex s1 =>
+ match toLatex l2 with
+ latex s2 =>
+ latex (s1 +++ s2)
+ end
+ end.
+Notation "a +=+ b" := (concatLatex a b) (at level 60, right associativity).
+
+
+