fact: Definition of_Z (x : Z) : option i63 := if (min_int 63 <=? x)%Z then if (x <? 0)%Z then Some (mk_i63 (Int63.of_Z (x + max_uint 63))) else if (x <? max_int 63)%Z then Some (mk_i63 (of_Z x)) else None else None.
imports: Coq(NArith ZArith Int63 Program.Wf)