Last change
on this file since 2731 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  

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  

Note: See
TracBrowser
for help on using the repository browser.