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