extracted/exp.ml

   1 open Preamble
   2
   3 open Bool
   4
   5 open Hints_declaration
   6
   7 open Core_notation
   8
   9 open Pts
  10
  11 open Logic
  12
  13 open Relations
  14
  15 open Nat
  16
  17 open Div_and_mod
  18
  19 (** val exp : Nat.nat -> Nat.nat -> Nat.nat **)
  20 let rec exp n = function
  21 | Nat.O -> Nat.S Nat.O
  22 | Nat.S p -> Nat.times (exp n p) n
  23