source: src/joint/String.ma @ 3362

Last change on this file since 3362 was 2647, checked in by sacerdot, 7 years ago

Stupid typo fixed.

File size: 221 bytes
RevLine 
[2645]1include "basics/pts.ma".
[475]2
[2645]3(* Stupid definition, just to avoid an axiom in the extracted code *)
4(* Strings at the moment are only used in comments in the back-end *)
[2647]5inductive String: Type[0] ≝
[2645]6   EmptyString : String.
Note: See TracBrowser for help on using the repository browser.