extracted/coqlib.ml

   1 open Preamble
   2
   3 open Hints_declaration
   4
   5 open Core_notation
   6
   7 open Pts
   8
   9 open Logic
  10
  11 open Types
  12
  13 open Bool
  14
  15 open Relations
  16
  17 open Nat
  18
  19 open List
  20
  21 open Div_and_mod
  22
  23 open Jmeq
  24
  25 open Russell
  26
  27 open Util
  28
  29 (** val align : Nat.nat -> Nat.nat -> Nat.nat **)
  30 let align n amount =
  31   Nat.times
  32     (Util.division (Nat.minus (Nat.plus n amount) (Nat.S Nat.O)) amount)
  33     amount
  34