fact: Definition int_to_trunc_index@{} (v : Decimal.int) : option trunc_index := match v with | Decimal.Pos d => Some (nat_to_trunc_index (Nat.of_uint d)) | Decimal.Neg d => match Nat.of_uint d with | 2%nat => Some minus_two | 1%nat => Some (minus_two.+1) | 0%nat => Some (minus_two.+2) | _ => None end end.
imports: Basics.Overture Basics.Contractible Basics.Equivalences Basics.Tactics Basics.Nat