include "basics/pts.ma".

(* Stupid definition, just to avoid an axiom in the extracted code *)
(* Strings at the moment are only used in comments in the back-end *)
inductive String: Type[0] ≝
   EmptyString : String.