chapter \Generated by Lem from \num_extra.lem\.\ theory "Lem_num_extra" imports Main "Lem_num" "Lem_string" begin (* **************************************************** *) (* *) (* A library of additional functions on numbers *) (* *) (* **************************************************** *) (*open import Num*) (*open import String*) (*val naturalOfString : string -> natural*) (*val integerOfString : string -> integer*) (* Truncation integer division (round toward zero) *) (*val integerDiv_t: integer -> integer -> integer*) (* Truncation modulo *) (*val integerRem_t: integer -> integer -> integer*) (* Flooring modulo *) (*val integerRem_f: integer -> integer -> integer*) end