fact: Fixpoint of_list (l : list digits) : uint := match l with | nil => Nil | cons d0 l => D0 (of_list l) | cons d1 l => D1 (of_list l) | cons d2 l => D2 (of_list l) | cons d3 l => D3 (of_list l) | cons d4 l => D4 (of_list l) | cons d5 l => D5 (of_list l) | cons d6 l => D6 (of_list l) | cons d7 l => D7 (of_list l) | cons d8 l => D8 (of_list l) | cons d9 l => D9 (of_list l) end.
imports: Decimal Arith ZArith