fact: Definition StrictTerminal_Format : FormatM S T := fun a env => t <- {t | bin_measure t = 0}; ret (t, env).
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Computation Fiat.Narcissus.Common.Specs