text: #ifndef PQCLEAN_SNTRUP857_AVX2_CRYPTO_ENCODE_857X1723_H
  #define PQCLEAN_SNTRUP857_AVX2_CRYPTO_ENCODE_857X1723_H
  
  #include <stdint.h>
  #define PQCLEAN_SNTRUP857_AVX2_crypto_encode_857x1723_STRBYTES 1152
  #define PQCLEAN_SNTRUP857_AVX2_crypto_encode_857x1723_ITEMS 857
  #define PQCLEAN_SNTRUP857_AVX2_crypto_encode_857x1723_ITEMBYTES 2
  
  void PQCLEAN_SNTRUP857_AVX2_crypto_encode_857x1723(unsigned char *out, const void *v);
  #endif
  