#include <wctype.h>
typedef int                                                              wint_t;

/*
STDC(199409)
*/