Changeset 2717 for extracted/util.mli


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.mli

    r2601 r2717  
    182182  Nat.nat -> Nat.nat -> (Nat.nat, Nat.nat) Types.prod
    183183
    184 val exponential : Nat.nat -> Nat.nat -> Nat.nat
    185 
    186184val less_than_or_equal_b_elim :
    187185  Nat.nat -> Nat.nat -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
    188186
    189187open Div_and_mod
    190 
    191 type even_p = __
    192 
    193 type odd_p = __
    194188
    195189val if_then_else_safe : Bool.bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
Note: See TracChangeset for help on using the changeset viewer.