Changeset 2717 for extracted/util.ml


Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (7 years ago)
Author:
sacerdot
Message:

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:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/util.ml

    r2601 r2717  
    554554  { Types.fst = (division m n); Types.snd = (modulus m n) }
    555555
    556 (** val exponential : Nat.nat -> Nat.nat -> Nat.nat **)
    557 let rec exponential m = function
    558 | Nat.O -> Nat.S Nat.O
    559 | Nat.S o -> Nat.times m (exponential m o)
    560 
    561556(** val less_than_or_equal_b_elim :
    562557    Nat.nat -> Nat.nat -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     
    567562
    568563open Div_and_mod
    569 
    570 type even_p = __
    571 
    572 type odd_p = __
    573564
    574565(** val if_then_else_safe :
Note: See TracChangeset for help on using the changeset viewer.