source: extracted/exp.ml @ 2746

Last change on this file since 2746 was 2717, checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 268 bytes
Line 
1open Preamble
2
3open Bool
4
5open Hints_declaration
6
7open Core_notation
8
9open Pts
10
11open Logic
12
13open Relations
14
15open Nat
16
17open Div_and_mod
18
19(** val exp : Nat.nat -> Nat.nat -> Nat.nat **)
20let rec exp n = function
21| Nat.O -> Nat.S Nat.O
22| Nat.S p -> Nat.times (exp n p) n
23
Note: See TracBrowser for help on using the repository browser.