Exhaustivity checks lets non exhaustive case fail later
When running why3 prove -L . modulo.mlw there is a non exhaustivity error during VC generation. It as not been detected during typing of q.mlw. --debug no_vc_eval could be needed otherwise the error appears somewhere else.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information