let s_real = HString.mk_hstring "real"